PLIF PLATFORM: MODELING AND VERIFICATION OF INFORMATION FLOWS IN SOFTWARE DB UNITS USING THE TEMPORAL LOGIC OF ACTIONS TLA+

Capa

Citar

Texto integral

Acesso aberto Acesso aberto
Acesso é fechado Acesso está concedido
Acesso é fechado Acesso é pago ou somente para assinantes

Resumo

The verification of software properties using formal verification tools is one of the current research directions in the field of information flow control. Security conditions of information flows in software under various information noninterferrence schemes are naturally described by so-called hyper-properties in well-known extensions of linear temporal logic and computation tree logic. In practice, verifying such properties for large projects is a non-trivial task. In this work, the authors translate the idea of dynamic type checking to detect prohibited information flows into the realm of computation verification using model-checking tools. Computations over security labels (safe types) are described by the abstract semantics of information flows. Transitioning from concrete computational semantics to abstract semantics of information flows allows formulating these security properties as state properties. In this case, proven tools in large industrial projects such as TLA+ and TLC can be used for the description and verification of real computer systems.

Sobre autores

A. Timakov

MIREA – Russian Technological University

Email: timakov@mirea.ru
78 Vernadsky Avenue, Moscow 119454

I. Ryzhov

RUDN University

Email: ryzhov.ilgen@gmail.com
6 Miklukho-Maklaya street, Moscow, 117198, Russia

Bibliografia

  1. Timakov A.А. Analysis of information flow security using software implementing business logic based on stored database program blocks. Russian Technological Journal. 2024. V. 12. № 2. P. 16–27.
  2. Тимаков А.А. PLIF. 2021. GitHub. https://github.com / timimin / plif
  3. Kozyri E. et al. Expressing Information Flow Properties // Foundations and Trends® in Privacy and Security. 2022. V. 3. № 1. P. 1–102.
  4. Hedin D., Sabelfeld A. A Perspective on Information-Flow Control // Software safety and security. 2012. P. 319–347.
  5. Balliu M., Schoepe D., Sabelfeld A. We are family: Relating information-flow trackers // Computer Security – ESORICS 2017: 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11–15, 2017, Proceedings, Part I 22. Springer International Publishing. 2017. P. 124–145.
  6. Russo A., Sabelfeld A., Li K. Implicit flows in malicious and nonmalicious code // Logics and Languages for Reliability and Security. – IOS Press, 2010. P. 301–322.
  7. Jang D. et al. An empirical study of privacy-violating information flows in JavaScript web applications // Proceedings of the 17th ACM conference on Computer and communications security. 2010. P. 270–283.
  8. Kang M.G. et al. Dta++: dynamic taint analysis with targeted control-flow propagation // NDSS. 2011.
  9. King D. et al. Implicit flows: Can’t live with ‘em, can’t live without ‘em // Information Systems Security: 4th International Conference, ICISS 2008, Hyderabad, India, December 16–20, 2008. Proceedings 4. Springer Berlin Heidelberg, 2008. P. 56–70.
  10. Staicu C.A. et al. An empirical study of information flows in real-world javascript // Proceedings of the 14th ACM SIGSAC Workshop on Programming Languages and Analysis for Security. 2019. P. 45–59.
  11. Myers C.A., Liskov B. A decentralized model for information flow control // ACM SIGOPS Operating Systems Review. 1997. № 5. P. 129–142.
  12. Broberg N., van Delft B., Sands D. Paragon for practical programming with information-flow control // Programming Languages and Systems: 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Australia, December 9–11, 2013. Proceedings 11. Springer International Publishing. 2013. P. 217–232.
  13. Pottier F., Simonet V. Information Flow Inference for ML // ACM Transactions on Programming Languages and Systems. 2003. P. 117–158.
  14. Volpano D., Irvine C., Smith G. Sound type system for secure flow analysis // Journal of Computer Security. 1996. № 2–3. P. 167–187.
  15. Clarkson M.R. et al. Temporal logics for hyperproperties // Principles of Security and Trust: Third International Conference, POST 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5–13. 2014. Proceedings 3. Springer Berlin Heidelberg. 2014. P. 265–284.
  16. Spearritt J. // Thesis for the Degree of Doctor of Engineering Practical. The Applicability of Information Flow to Secure Java Development, 2017.
  17. Seifermann S. et al. Detecting violations of access control and information flow policies in data flow diagrams // Journal of Systems and Software. 2022. V. 184. P. 111138.
  18. Methni A., Lemerre M., Hedia B.B., Barkaoui K., Haddad S. An Approach for Verifying Concurrent C Programs // 8th Junior Researcher Workshop on Real-Time Computing. 2014. P. 33–36.
  19. Lamport L. Specifying systems: the TLA+ language and tools for hardware and software engineers. 2002.
  20. Becker S., Koziolek H., Reussner R. The Palladio component model for model-driven performance prediction // Journal of Systems and Software. 2009. V. 82. № 1. P. 3–22.
  21. Dura A., Reichenbach C., Sŏderberg E. JavaDL: automatically incrementalizing Java bug pattern detection // Proceedings of the ACM on Programming Languages. 2021. V. 5. № OOPSLA. P. 1–31.
  22. Leavens G.T., Baker A.L., Ruby C. JML: a Java modeling language // Formal Underpinnings of Java Workshop (at OOPSLA’98). 1998. P. 404–420.
  23. Harel D., Kozen D., Tiuryn J. Dynamic logic // ACM SIGACT News. 2001. V. 32. № 1. P. 66–69.
  24. Ahrendt W. et al. The KeY platform for verification and analysis of Java programs // Verified Software: Theories, Tools and Experiments: 6th International Conference, VSTTE 2014, Vienna, Austria, July 17–18, 2014, Revised Selected Papers 6. Springer International Publishing. 2014. P. 55–71.
  25. DeMarco T. Structured analysis and system specification. Software pioneers: contributions to software engineering. Berlin, Heidelberg: Springer Berlin Heidelberg. 2011. P. 529–560.

Arquivos suplementares

Arquivos suplementares
Ação
1. JATS XML
Baixar

Declaração de direitos autorais © Russian Academy of Sciences, 2025