Возможности статической верификации монолитного ядра операционных систем
https://doi.org/10.15514/ISPRAS-2017-29(2)-4
Аннотация
Список литературы
1. В.Е. Карпов, К.А. Коньков. Основы операционных систем. Курс лекций. Учебное пособие. М.: Интернет-университет информационных технологий, 536 с., 2005.
2. Е.М. Новиков. Развитие ядра операционной системы Linux. Труды ИСП РАН, т. 29, вып. 2, 2017, стр. xx-xx. DOI: 10.15514/ISPRAS-2017-29(2)-3
3. R.L. Glass. Facts and fallacies of software engineering. Addison-Wesley Professional, 2002.
4. J. Corbet, G. Kroah-Hartman. Linux kernel development. How Fast It is Going, Who is Doing It, What They Are Doing and Who is Sponsoring the Work. http://go.linuxfoundation.org/linux-kernel-development-report-2016, 2016.
5. А.В. Цыварев, В.А. Мартиросян. Тестирование драйверов файловых систем в ОС Linux. Труды ИСП РАН, т. 23, 2012, стр. 413-426. DOI: 10.15514/ISPRAS-2012-23-24
6. J.-P. Lozi, B. Lepers, J. Funston, F. Gaud, V. Quéma, A. Fedorova. The Linux scheduler: a decade of wasted cores. In Proceedings of the Eleventh European Conference on Computer Systems (EuroSys '16), article 1, 16 pages, 2016.
7. A. Chou, J. Yang, B. Chelf, S. Hallem, D. Engler. An empirical study of operating systems errors. In Proceedings of the eighteenth ACM symposium on Operating systems principles (SOSP'01), pp. 73-88, 2001.
8. J.L. Lawall, J. Brunel, N. Palix, H.R. Rydhof, H. Stuart, G. Muller. WYSIWIB: A declarative approach to finding API protocols and bugs in Linux code. Proceedings of the 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), pp. 43-52, 2009.
9. А. Аветисян, А. Белеванцев, А. Бородин, В. Несов. Использование статического анализа для поиска уязвимостей и критических ошибок в исходном коде программ. Труды ИСП РАН, т. 21, 2011, стр. 23-38.
10. N. Palix, G. Thomas, S. Saha, C. Calves, J. Lawall, G. Muller. Faults in Linux: ten years later. In Proceedings of the 15th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS'11), pp. 305-318, 2011.
11. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, S. Winwood. seL4: formal verification of an OS kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP'09), pp. 207-220, 2009.
12. J. Andronick, D. Greenaway, K. Elphinstone. Towards proving security in the presence of large untrusted components. In Proceedings of the 5th international conference on Systems software verification (SSV'10), pp. 9-9, 2010.
13. G. Klein. From a verified kernel towards verified systems. In Proceedings of the 8th Asian conference on Programming languages and systems (APLAS'10), pp. 21-33, 2010.
14. I. Kuz, G. Klein, C. Lewis, A. Walker. capDL: a language for describing capability-based systems. In Proceedings of the first ACM asia-pacific workshop on Workshop on systems (APSys'10), pp. 31-36, 2010.
15. T. Sewell, S. Winwood, P. Gammie, T. Murray, J. Andronick, G. Klein. seL4 enforces integrity. In Proceedings of the Second international conference on Interactive theorem proving (ITP'11), pp. 325-340, 2011.
16. T. Murray, D. Matichuk, M. Brassil, P. Gammie, G. Klein. Noninterference for operating system kernels. In Proceedings of the Second international conference on Certified Programs and Proofs (CPP'12), pp. 126-142, 2012.
17. M. Daum, N. Billing, G. Klein. Concerned with the unprivileged: user programs in kernel refinement. Formal Aspects of Computing, vol. 26, issue 6, pp. 1205-1229, 2014.
18. G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, G. Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems (TOCS), vol. 32, issue 1, 70 pages, 2014.
19. C. Baumann, B. Beckert, H. Blasum, T. Bormer. Formal Verification of a Microkernel Used in Dependable Software Systems. In Proceedings of the 28th International Conference on Computer Safety, Reliability, and Security (SAFECOMP'09), pp. 187-200, 2009.
20. E. Alkassar, W. J. Paul, A. Starostin, A. Tsyban. Pervasive verification of an OS microkernel: inline assembly, memory consumption, concurrent devices. In Proceedings of the Third international conference on Verified software: theories, tools, experiments (VSTTE'10), pp. 71-85, 2010.
21. C. Baumann, T. Bormer, H. Blasum, S. Tverdyshev. Proving Memory Separation in a Microkernel by Code Level Verification. In Proceedings of the 14th IEEE International Symposium on Object/Component/Service-Oriented Real-Time Distributed Computing Workshops (ISORCW '11), pp. 25-32, 2011.
22. S. Schmaltz, A. Shadrin. Integrated semantics of intermediate-language c and macro-assembler for pervasive formal verification of operating systems and hypervisors from VerisoftXT. In Proceedings of the 4th international conference on Verified Software: theories, tools, experiments (VSTTE'12), pp. 18-33, 2012.
23. R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. Wu, S.-C. Weng, H. Zhang, Y. Guo. Deep Specifications and Certified Abstraction Layers. SIGPLAN Not. 50, 1, pp. 595-608, 2015.
24. M. Děcký. A road to a formally verified general-purpose operating system. In Proceedings of the First international conference on Architecting Critical Systems (ISARCS'10), pp. 72-88, 2010.
25. H. Mai, E. Pek, H. Xue, S. T. King, P. Madhusudan. Verifying security invariants in ExpressOS. In Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems (ASPLOS '13), pp. 293-304, 2013.
26. J.F. Ferreira, C. Gherghina, G. He, S. Qin, W.-N. Chin. Automated verification of the FreeRTOS scheduler in Hip/Sleek. Int. J. Softw. Tools Technol. Transf. 16, 4, pp. 381-397, 2014.
27. A. Gotsman, H. Yang. Modular verification of preemptive OS kernels. In Proceedings of the 16th ACM SIGPLAN international conference on Functional programming (ICFP '11), pp. 404-417, 2011.
28. J. Yang, Chris Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '10), pp. 99-110, 2010.
29. M. Danish, H. Xi. Operating system development with ATS: work in progress. In Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification (PLPV'10), pp. 9-14, 2010.
30. M. Danish, H. Xi. Using Lightweight Theorem Proving in an Asynchronous Systems Context. In Proceedings of the 6th International Symposium on NASA Formal Methods, vol. 8430, pp. 158-172. 2014.
31. B.W. Cronkite-Ratcliff. Development of automatically verifiable systems using data representation synthesis. In Proceedings of the 2013 companion publication for conference on Systems, programming, & applications: software for humanity (SPLASH '13), pp. 109-110, 2013.
32. K.R.M. Leino. Developing verified programs with dafny. In Proceedings of the 2013 International Conference on Software Engineering (ICSE '13), pp. 1488-1490, 2013.
33. A. DeHon, B. Karel, T. F. Knight, Jr., G. Malecha, B. Montagu, R. Morisset, G. Morrisett, B. C. Pierce, R. Pollack, S. Ray, O. Shivers, J. M. Smith, G. Sullivan. Preliminary design of the SAFE platform. In Proceedings of the 6th Workshop on Programming Languages and Operating Systems (PLOS '11), article 4, 5 pages, 2011.
34. A. Azevedo de Amorim, N. Collins, A. DeHon, D. Demange, C. Hriţcu, D. Pichardie, B. C. Pierce, R. Pollack, A. Tolmach. A verified information-flow architecture. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'14), pp. 165-178, 2014.
35. T. Ball, E. Bounimova, R. Kumar, V. Levin. SLAM2: Static driver verification with under 4% false alarms. In Proceedings of the 10th International Conference on Conference on Formal Methods in Computer-Aided Design (FMCAD'10), pp. 35-42, 2010.
36. D. Beyer. Status Report on Software Verification (Competition Summary SV-COMP 2014). In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS'14), LNCS 8413, pp. 373-388, 2014.
37. D. Beyer. Software Verification and Verifiable Witnesses (Report on SV-COMP 2015). In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and of Analysis Systems (TACAS'15), LNCS 9035, pp. 401-416, 2015.
38. T. Ball, V. Levin, S.K. Rajamani. A decade of software model checking with SLAM. Communications of the ACM, vol. 54, issue 7, pp. 68-76, 2011.
39. T. Witkowski, N. Blanc, D. Kroening, G. Weissenbacher. Model checking concurrent Linux device drivers. In Proceedings of the 22nd IEEE/ACM international conference on Automated Software Engineering (ASE'07), pp. 501-504, 2007.
40. H. Post, W. Küchlin. Integrated static analysis for Linux device driver verification. In Proceedings of the 6th International Conference on Integrated Formal Methods (IFM'07), LNCS, vol. 4591, pp. 518-537, 2007.
41. Д. Бейер, А.К. Петренко. Верификация драйверов операционной системы Linux. Труды ИСП РАН, т. 23, стр. 405-412, 2012. DOI: 10.15514/ISPRAS-2012-23-23
42. И.С. Захаров, М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов. Конфигурируемая система статической верификации модулей ядра операционных систем. Программирование, т. 41, выпуск 1, стр. 44-67, 2015.
43. T. Ströder, C. Aschermann, F. Frohn, J. Hensel, J. Giesl. AProVE: Termination and Memory Safety of C Programs (Competition Contribution). In Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), LNCS 9035, pp. 417-419, 2015.
44. M. Kotoun, P. Peringer, V. Šoková, T. Vojnar. Optimized PredatorHP and the SV-COMP Heap and Memory Safety Benchmark. In Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), vol. 9636, pp. 942-945, 2016.
45. D. Engler, M. Musuvathi. Static analysis versus model checking for bug finding. In Proceedings of the 5th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'04), LNCS, vol. 2937, pp. 191-210, 2004.
46. T. Ball, S.K. Rajamani. SLIC: A specification language for interface checking of C. Technical Report MSR-TR-2001-21, Microsoft Research, 2001.
47. Е.М. Новиков. Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы Linux. Диссертация на соискание ученой степени кандидата физико-математических наук, Институт системного программирования РАН, 2013.
48. A. Khoroshilov, V. Mutilin, E. Novikov, I. Zakharov. Modeling Environment for Static Verification of Linux Kernel Modules. In Proceedings of the 9th International Ershov Informatics Conference (PSI'14), LNCS 8974, pages 400-414, 2014.
Рецензия
Для цитирования:
Новиков Е.М. Возможности статической верификации монолитного ядра операционных систем. Труды Института системного программирования РАН. 2017;29(2):97-116. https://doi.org/10.15514/ISPRAS-2017-29(2)-4
For citation:
Novikov E.M. Static verification of operating system monolithic kernels. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(2):97-116. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(2)-4
Послать статью по эл. почте 