[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Formalization and Analysis of Aeolus-based File System from Process Algebra Perspective

  • Research
  • Published:
Mobile Networks and Applications Aims and scope Submit manuscript

Abstract

The secure transmission of information is receiving more and more attention nowadays. Aeolus is a novel platform designed to enhance the development of distributed applications by preventing unauthorized disclosure of information. And one of the most representative systems for information transmission is the file system, therefore it is of great significance to formally analyze the Aeolus-based file system. In this paper, we use Communicating Sequential Processes (CSP) to model and formalize the file system based on Aeolus. Moreover, we utilize the Process Analysis Toolkit (PAT) to simulate and verify the CSP description of our established model. We specifically verify the validity of five properties: Deadlock Freedom, Divergence Freedom, Reachability, Secrecy, and Integrity. The verification results demonstrate that the model successfully satisfies these properties, affirming the effectiveness of the framework in ensuring file operations and guaranteeing the secure transmission of information.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Data Availability

No datasets were generated or analysed during the current study.

References

  1. Cheng WWY (2009) Information flow for secure distributed applications. PhD thesis, Massachusetts Institute of Technology

  2. 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’06). IEEE, pp 350–364

  3. 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–366

  4. Dalton M, Kannan H, Kozyrakis C (2007) Raksha: a flexible information flow architecture for software security. ACM SIGARCH Comput Archit News 35(2):482–493

    Article  Google Scholar 

  5. Denning DE (1976) A lattice model of secure information flow. Commun of the ACM 19(5):236–243

    Article  MathSciNet  Google Scholar 

  6. Denning DER (1982) Cryptography and data security, vol 112. Addison-Wesley Reading

  7. 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–30

    Article  Google Scholar 

  8. Failures divergences refinement: FDR2 manual (2005) Formal systems (europe) ltd. http://www.fsel.com

  9. 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–36

    Article  MathSciNet  Google Scholar 

  10. Garfinkel T, Pfaff B, Rosenblum M, et al (2004) Ostia: A delegating architecture for secure system call interposition. In: NDSS

  11. Hoare CAR (1978) Communicating sequential processes. Commun of the ACM 21(8):666–677

    Article  Google Scholar 

  12. Hou Z, Yin J, Zhu H (2021) Formalization and verification of dubbo using csp. In: SEKE. pp 154–159

  13. 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–76

  14. 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–334

    Article  Google Scholar 

  15. Krohn MN (2008) Information flow control for secure web sites. PhD thesis, Massachusetts Institute of Technology

  16. Lampson BW (1973) A note on the confinement problem. Commun ACM 16(10):613–615

    Article  Google Scholar 

  17. Li W, Yang Z, Liu J (2022) Automatic analysis of difc systems using noninterference with declassification. Neural computing and applications. pp 1–12

  18. Lowe G, Roscoe B (1997) Using csp to detect errors in the tmn protocol. IEEE Trans Softw Eng 23(10):659–669

    Article  Google Scholar 

  19. McKee FP (2011) A file system design for the Aeolus security platform. Massachusetts Institute of Technology

  20. 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–241

  21. Myers AC, Liskov B (1997) A decentralized model for information flow control. ACM SIGOPS Oper Syst Rev 31(5):129–142

    Article  Google Scholar 

  22. Myers AC, Chong S, Nystrom N, Zheng L, Zdancewic S (2001) Jif: Java information flow. http://www.cs.cornell.edu/jif

  23. PAT (2023) [Online] Available. http://pat.comp.nus.edu.sg/

  24. Popic V (2010) Audit trails in the Aeolus distributed security platform. Massachusetts Institute of Technology

  25. Roscoe A, Huang J (2013) Checking noninterference in timed csp. Formal Asp Comput 25(1):3–35

    Article  MathSciNet  Google Scholar 

  26. 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–74

  27. Sabelfeld A, Myers AC (2003) Language-based information-flow security. IEEE J Sel Areas Commun 21(1):5–19

    Article  Google Scholar 

  28. States U (1987) Department of Defense Trusted Computer System Evaluation Criteria, vol 83. Department of Defense

  29. Suh GE, Lee JW, Zhang D, Devadas S (2004) Secure program execution via dynamic information flow tracking. ACM Sigplan Not 39(11):85–96

  30. 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

    Article  Google Scholar 

  31. 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–16

    Article  Google Scholar 

  32. 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 28

  33. 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

    Google Scholar 

  34. 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

    Google Scholar 

  35. 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–246

  36. Zeldovich N (2008) Securing untrustworthy software using information flow control. Stanford University

  37. Zeldovich N, Boyd-Wickizer S, Mazieres D (2008) Securing distributed systems with information flow control. NSDI 8:293–308

    Google Scholar 

  38. Zeldovich N, Boyd-Wickizer S, Kohler E, Mazieres D (2011) Making information flow explicit in histar. Commun ACM 54(11):93–101

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China

    Zhiru Hou & Huibiao Zhu

  2. Donghua University, Shanghai, China

    Lili Xiao

  3. Nguyen Tat Thanh University, 300A Nguyen Tat Thanh Street, Ward 13, District 4, Ho Chi Minh City, Vietnam

    Phan Cong Vinh

Authors
  1. Zhiru Hou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lili Xiao
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Huibiao Zhu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Phan Cong Vinh
    View author publications

    You can also search for this author in PubMed Google Scholar

Contributions

Zhiru Hou conducted the research, and drafted the main manuscript. Huibiao Zhu provided valuable contributions to the methodology of this study, and made critical modifications to the manuscript. Lili Xiao and Phan Cong Vinh contributed to data analysis through insightful discussions and analysis.

Corresponding authors

Correspondence to Huibiao Zhu or Phan Cong Vinh.

Ethics declarations

Competing interests

The authors declare no competing interests.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Hou, Z., Xiao, L., Zhu, H. et al. Formalization and Analysis of Aeolus-based File System from Process Algebra Perspective. Mobile Netw Appl 29, 273–285 (2024). https://doi.org/10.1007/s11036-024-02332-w

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11036-024-02332-w

Keywords

Search

Navigation