{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,7]],"date-time":"2026-06-07T04:48:51Z","timestamp":1780807731530,"version":"3.54.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T00:00:00Z","timestamp":1706745600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T00:00:00Z","timestamp":1706745600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2024,2]]},"DOI":"10.1007\/s11036-024-02332-w","type":"journal-article","created":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T15:10:36Z","timestamp":1726240236000},"page":"273-285","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalization and Analysis of Aeolus-based File System from Process Algebra Perspective"],"prefix":"10.1007","volume":"29","author":[{"given":"Zhiru","family":"Hou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lili","family":"Xiao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Phan Cong","family":"Vinh","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"2332_CR1","unstructured":"Cheng WWY (2009) Information flow for secure distributed applications. PhD thesis, Massachusetts Institute of Technology"},{"key":"2332_CR2","doi-asserted-by":"crossref","unstructured":"Cox RS, Hansen JG, Gribble SD, Levy HM (2006) A safety-oriented platform for web applications. In: 2006 IEEE symposium on security and privacy (S &P\u201906). IEEE, pp 350\u2013364","DOI":"10.1109\/SP.2006.4"},{"key":"2332_CR3","doi-asserted-by":"crossref","unstructured":"Criswell J, Lenharth A, Dhurjati D, Adve V (2007) Secure virtual architecture: A safe execution environment for commodity operating systems. In: Proceedings of twenty-first ACM SIGOPS symposium on Operating systems principles. pp 351\u2013366","DOI":"10.1145\/1323293.1294295"},{"issue":"2","key":"2332_CR4","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1145\/1273440.1250722","volume":"35","author":"M Dalton","year":"2007","unstructured":"Dalton M, Kannan H, Kozyrakis C (2007) Raksha: a flexible information flow architecture for software security. ACM SIGARCH Comput Archit News 35(2):482\u2013493","journal-title":"ACM SIGARCH Comput Archit News"},{"issue":"5","key":"2332_CR5","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"DE Denning","year":"1976","unstructured":"Denning DE (1976) A lattice model of secure information flow. Commun of the ACM 19(5):236\u2013243","journal-title":"Commun of the ACM"},{"key":"2332_CR6","unstructured":"Denning DER (1982) Cryptography and data security, vol 112. Addison-Wesley Reading"},{"issue":"5","key":"2332_CR7","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1095809.1095813","volume":"39","author":"P Efstathopoulos","year":"2005","unstructured":"Efstathopoulos P, Krohn M, VanDeBogart S, Frey C, Ziegler D, Kohler E, Mazieres D, Kaashoek F, Morris R (2005) Labels and event processes in the asbestos operating system. ACM SIGOPS Oper Syst Rev 39(5):17\u201330","journal-title":"ACM SIGOPS Oper Syst Rev"},{"key":"2332_CR8","unstructured":"Failures divergences refinement: FDR2 manual (2005) Formal systems (europe) ltd. http:\/\/www.fsel.com"},{"issue":"4","key":"2332_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3599731","volume":"35","author":"Y Fei","year":"2023","unstructured":"Fei Y, Zhu H, Yin J (2023) Fvf-aka: A formal verification framework of aka protocols for multi-server iot. Formal Asp Comput 35(4):1\u201336","journal-title":"Formal Asp Comput"},{"key":"2332_CR10","unstructured":"Garfinkel T, Pfaff B, Rosenblum M, et\u00a0al (2004) Ostia: A delegating architecture for secure system call interposition. In: NDSS"},{"issue":"8","key":"2332_CR11","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare CAR (1978) Communicating sequential processes. Commun of the ACM 21(8):666\u2013677","journal-title":"Commun of the ACM"},{"key":"2332_CR12","doi-asserted-by":"crossref","unstructured":"Hou Z, Yin J, Zhu H (2021) Formalization and verification of dubbo using csp. In: SEKE. pp 154\u2013159","DOI":"10.18293\/SEKE2021-077"},{"key":"2332_CR13","doi-asserted-by":"crossref","unstructured":"Krohn M, Tromer E (2009) Noninterference for a practical difc-based operating system. In: 2009 30th IEEE symposium on security and privacy. IEEE, pp 61\u201376","DOI":"10.1109\/SP.2009.23"},{"issue":"6","key":"2332_CR14","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/1323293.1294293","volume":"41","author":"M Krohn","year":"2007","unstructured":"Krohn M, Yip A, Brodsky M, Cliffer N, Kaashoek MF, Kohler E, Morris R (2007) Information flow control for standard os abstractions. ACM SIGOPS Oper Syst Rev 41(6):321\u2013334","journal-title":"ACM SIGOPS Oper Syst Rev"},{"key":"2332_CR15","unstructured":"Krohn MN (2008) Information flow control for secure web sites. PhD thesis, Massachusetts Institute of Technology"},{"issue":"10","key":"2332_CR16","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1145\/362375.362389","volume":"16","author":"BW Lampson","year":"1973","unstructured":"Lampson BW (1973) A note on the confinement problem. Commun ACM 16(10):613\u2013615","journal-title":"Commun ACM"},{"key":"2332_CR17","doi-asserted-by":"crossref","unstructured":"Li W, Yang Z, Liu J (2022) Automatic analysis of difc systems using noninterference with declassification. Neural computing and applications. pp 1\u201312","DOI":"10.1007\/s00521-021-06334-7"},{"issue":"10","key":"2332_CR18","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G Lowe","year":"1997","unstructured":"Lowe G, Roscoe B (1997) Using csp to detect errors in the tmn protocol. IEEE Trans Softw Eng 23(10):659\u2013669","journal-title":"IEEE Trans Softw Eng"},{"key":"2332_CR19","unstructured":"McKee FP (2011) A file system design for the Aeolus security platform. Massachusetts Institute of Technology"},{"key":"2332_CR20","doi-asserted-by":"crossref","unstructured":"Myers AC (1999) Jflow: Practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp 228\u2013241","DOI":"10.1145\/292540.292561"},{"issue":"5","key":"2332_CR21","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/269005.266669","volume":"31","author":"AC Myers","year":"1997","unstructured":"Myers AC, Liskov B (1997) A decentralized model for information flow control. ACM SIGOPS Oper Syst Rev 31(5):129\u2013142","journal-title":"ACM SIGOPS Oper Syst Rev"},{"key":"2332_CR22","unstructured":"Myers AC, Chong S, Nystrom N, Zheng L, Zdancewic S (2001) Jif: Java information flow. http:\/\/www.cs.cornell.edu\/jif"},{"key":"2332_CR23","unstructured":"PAT (2023) [Online] Available. http:\/\/pat.comp.nus.edu.sg\/"},{"key":"2332_CR24","unstructured":"Popic V (2010) Audit trails in the Aeolus distributed security platform. Massachusetts Institute of Technology"},{"issue":"1","key":"2332_CR25","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-012-0251-6","volume":"25","author":"A Roscoe","year":"2013","unstructured":"Roscoe A, Huang J (2013) Checking noninterference in timed csp. Formal Asp Comput 25(1):3\u201335","journal-title":"Formal Asp Comput"},{"key":"2332_CR26","doi-asserted-by":"crossref","unstructured":"Roy I, Porter DE, Bond MD, McKinley KS, Witchel E (2009) Laminar: Practical fine-grained decentralized information flow control. In: Proceedings of the 30th ACM SIGPLAN conference on programming language design and implementation. pp 63\u201374","DOI":"10.1145\/1542476.1542484"},{"issue":"1","key":"2332_CR27","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld A, Myers AC (2003) Language-based information-flow security. IEEE J Sel Areas Commun 21(1):5\u201319","journal-title":"IEEE J Sel Areas Commun"},{"key":"2332_CR28","unstructured":"States U (1987) Department of Defense Trusted Computer System Evaluation Criteria, vol\u00a083. Department of Defense"},{"key":"2332_CR29","doi-asserted-by":"crossref","unstructured":"Suh GE, Lee JW, Zhang D, Devadas S (2004) Secure program execution via dynamic information flow tracking. ACM Sigplan Not 39(11):85\u201396","DOI":"10.1145\/1037187.1024404"},{"issue":"4","key":"2332_CR30","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/1314299.1314302","volume":"25","author":"S Vandebogart","year":"2007","unstructured":"Vandebogart S, Efstathopoulos P, Kohler E, Krohn M, Frey C, Ziegler D, Kaashoek F, Morris R, Mazieres D (2007) Labels and event processes in the asbestos operating system. ACM Trans Comput Syst (TOCS) 25(4):11","journal-title":"ACM Trans Comput Syst (TOCS)"},{"issue":"6","key":"2332_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1323293.1294263","volume":"41","author":"HJ Wang","year":"2007","unstructured":"Wang HJ, Fan X, Howell J, Jackson C (2007) Protection and communication abstractions for web browsers in mashupos. ACM SIGOPS Oper Syst Rev 41(6):1\u201316","journal-title":"ACM SIGOPS Oper Syst Rev"},{"key":"2332_CR32","unstructured":"Wang HJ, Grier C, Moshchuk A, King ST, Choudhury P, Venter H (2009) The multi-principal os construction of the gazelle web browser. In: USENIX security symposium, vol\u00a028"},{"issue":"109","key":"2332_CR33","first-page":"843","volume":"232","author":"Z Wang","year":"2023","unstructured":"Wang Z, Zhang L, Guo R, Wang G, Qiu J, Su S, Liu Y, Xu G, Tian Z (2023) A covert channel over blockchain based on label tree without long waiting times. Comput Netw 232(109):843","journal-title":"Comput Netw"},{"issue":"102","key":"2332_CR34","first-page":"343","volume":"187","author":"S Xiang","year":"2020","unstructured":"Xiang S, Zhu H, Wu X, Xiao L, Bonsangue M, Xie W, Zhang L (2020) Modeling and verifying the topology discovery mechanism of openflow controllers in software-defined networks using process algebra. Sci Comput Program 187(102):343","journal-title":"Sci Comput Program"},{"key":"2332_CR35","doi-asserted-by":"crossref","unstructured":"Yip A, Narula N, Krohn M, Morris R (2009) Privacy-preserving browser-side scripting with bflow. In: Proceedings of the 4th ACM European conference on Computer systems, pp 233\u2013246","DOI":"10.1145\/1519065.1519091"},{"key":"2332_CR36","unstructured":"Zeldovich N (2008) Securing untrustworthy software using information flow control. Stanford University"},{"key":"2332_CR37","first-page":"293","volume":"8","author":"N Zeldovich","year":"2008","unstructured":"Zeldovich N, Boyd-Wickizer S, Mazieres D (2008) Securing distributed systems with information flow control. NSDI 8:293\u2013308","journal-title":"NSDI"},{"issue":"11","key":"2332_CR38","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/2018396.2018419","volume":"54","author":"N Zeldovich","year":"2011","unstructured":"Zeldovich N, Boyd-Wickizer S, Kohler E, Mazieres D (2011) Making information flow explicit in histar. Commun ACM 54(11):93\u2013101","journal-title":"Commun ACM"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-024-02332-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11036-024-02332-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-024-02332-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,4]],"date-time":"2024-10-04T11:26:56Z","timestamp":1728041216000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11036-024-02332-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2]]},"references-count":38,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,2]]}},"alternative-id":["2332"],"URL":"https:\/\/doi.org\/10.1007\/s11036-024-02332-w","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"value":"1383-469X","type":"print"},{"value":"1572-8153","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,2]]},"assertion":[{"value":"19 April 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 September 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}