Integration Points of Operating System Verification Techniques
https://doi.org/10.15514/ISPRAS-2015-27(5)-10
Abstract
In this work the problem of high quality verification techniques applicable for operating systems is formulated. A perspective approach to solve this problem is integration of various verification methods. The solution technique can be considered successful if it allows to check the whole operating system and to verify in more accurate way the most important functions and components of the system, using more strict and formal methods for it. Based on the ISP RAS experience in operating system verification projects conducted using various verification techniques we determine development artefacts, that can be suitable integration point candidates for integration of formal specification based static and dynamic verification techniques for operating systems.
About the Authors
A. K. Petrenko
ISP RAS; Lomonosov Moscow State University; Moscow Institute of Physics and Technology; Higher School of Economics, National Research University
Russian Federation
Russian Federation
V. V. Kuliamin
ISP RAS; Lomonosov Moscow State University; Higher School of Economics, National Research University
Russian Federation
Russian Federation
A. V. Khoroshilov
ISP RAS; Lomonosov Moscow State University; Moscow Institute of Physics and Technology; Higher School of Economics, National Research University
Russian Federation
Russian Federation
References
1. Proceedings of the 1st International Conference on Integrated Formal Methods. Edited by K. Araki, A. Galloway, K. Taguchi, York, 28-29 June 1999. Springer-Verlag, 1999. ISBN:1-85233-107-0.
2. L. De Moura, N. Bjørner. Z3: an Efficient SMT Solver. Proceedings of TACAS’2008. LNCS 4963:337-340, Springer-Verlag, 2008.
3. http://github.com/Z3Prover/z3
4. C. Barret, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli. CVC4. Proceedings of CAV’2011, LNCS 6806:171-177, Springer, 2011.
5. http://cvc4.cs.nyuedu/web
6. M. Veanes, C. Campbell, W. Grieskamp, W. Schulte, N. Tillmann, L. Nachmanson. Model-based Testing of Object-oriented Reactive Systems with SpecExplorer. Proceedings of FORTEST’2008, LNCS 4949:39-76, Springer-Verlag, 2008.
7. N. Tillmann, J. de Halleux. Pex – White Box Test Generation for .NET. Proceedings of TAP’2008, LNCS 4966:134-153, Springer-Verlag, 2008.
8. P. Godefroid. Random Testing for Security: Blackbox vs. Whitebox Fuzzing. Proceedings of 2-nd International Workshop on Random Testing, p. 1-1, ACM, 2007.
9. T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Software Verification with BLAST. Proceedings of SPIN’2003, Model Checking Software, LNCS 2648:235-239, Springer-Verlag, 2003.
10. T. Ball, B. Cook, V. Levin, S. K. rajamani. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. Proceedings of IFM’2004, LNCS 2999:1-20, Springer-Verlag, 2004.
11. D. Beyer, M. E. Keremoglu. CPAchecker: a Tool for Configurable Software Verification. Proceedings of CAV’2011, LNCS 6806:184-190, Springer, 2011.
12. G. Canet, P. Cuoq, B. Monate. A Value Analysis for C Programs. Proceedings of SCAM’2009, p. 123-124, IEEE, 2009.
13. J.-R. Abrial, M. Butler, S. Hallerstede, L. Voisin. An Open Extensible Tool Environment for Event-B. Proceedings of ICFEM’2006, Formal Methods and Software Engineering, LNCS 4260:588-605, Springer-Verlag, 2006.
14. A. K. Petrenko. Unifikatsia v avtomotizatsii testirovania. Positsia UniTESK [Testing Unification and Automation. UniTESK Viewpoint]. Trudy ISP RAN [The Proceedings of ISP RAS], vol. 14(1):7-22, 2008 (in Russian).
15. V. V. Kuliamin. Integration of Software Verification Methods. Programming and Computer Software, 35(4):41-55, 2009. DOI 10.1134/S0361768809040057
16. V. V. Kuliamin. Software Verification Methods. Paper on Analytical Survey Contest on Information and Communication Systems, 2008 (http://www.ispras.ru/publications/2008/methods_of_software_verification/, in Russian).
17. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. Counterexample-Guided Abstraction Refinement. Proceedings of CAV’2000, LNCS 1855:154-169, Springer-Verlag, 2000.
18. Khoroshilov A.V., Mandrykin M. U., MutilinV. S. Vvedenie v metod CEGAR — utochnenie abstrakcii po kontrprimeram [Introduction to CEGAR — Counter-Example Guided Abstraction Refinement]. Trudy ISP RАN [The Proceedings of ISP RAS], vol. 24, pp. 219-292, 2013 (in Russian). DOI: 10.15514/ISPRAS-2013-24-12
19. V. V. Kuliamin, A. K. Petrenko. Razvitie Podkhoda k Razrabotke Testov UniTESK [Evolution of UniTESK Test Development Approach]. Trudy ISP RAN [The Proceedings of ISP RAS], vol. 26(1):9-26, 2014 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-1
20. A. V. Khoroshilov, M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. K. Petrenko, and I. S. Zakharov. Configurable toolset for static verification of operating systems kernel modules. Programming and Computer Software 41(1):49-64, 2015. DOI 10.1134/S0361768815010065
21. E. M. Novikov. Development of Software Contracts for Verification of Linux Operating System Kernel Modules. PhD Thesis, Moscow, 2013 (in Russian).
22. A. V. Khoroshilov, V. S. Mutilin, I. S. Zakharov. Pattern-based environment modeling for static verification of Linux kernel modules. Programming and Computer Software 41(3):183-195, 2015. DOI 10.1134/S036176881503007X
23. P. N. Devyanin, A. V. Khoroshilov, V. V. Kuliamin, A. K. Petrenko, and I. V. Shchepetkov. Using Refinement in Formal Development of OS Security Model. Proceedings of PSI’2015.
24. P. N. Devyanin. The role DP-model of access and information flows control in operating systems of Linux sets. Prikladnaia i Diskretnaia Matematika (Applied and Discrete Mathematics), 2012, № 1, 69–90 (in Russian).
Review
For citations:
Petrenko A.K., Kuliamin V.V., Khoroshilov A.V. Integration Points of Operating System Verification Techniques. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(5):175-190. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(5)-10
Email this article 