Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning
Published in: Journal of Automated Reasoning 1-4/2018

23-12-2017

Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

Authors: Hao Chen, Xiongnan Wu, Zhong Shao, Joshua Lockerman, Ronghui Gu

Published in: Journal of Automated Reasoning | Issue 1-4/2018

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified general-purpose kernels, but it is unclear how to extend their work to verify the functional correctness of device drivers, due to the non-local effects of interrupts. In this paper, we present a novel compositional framework for building certified interruptible OS kernels with device drivers. We provide a general device model that can be instantiated with various hardware devices, and a realistic formal model of interrupts, which can be used to reason about interruptible code. We have realized this framework in the Coq proof assistant. To demonstrate the effectiveness of our new approach, we have successfully extended an existing verified non-interruptible kernel with our framework and turned it into an interruptible kernel with verified device drivers. To the best of our knowledge, this is the first verified interruptible operating system with device drivers.
previous article CoSMed: A Confidentiality-Verified Social Media Platform
next article Verified iptables Firewall Analysis and Verification

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Footnotes
1
We have chosen the prefix form over the subset to allow us determine more easily where the current execution is at on the global event list.
 
2
In our IC model, the middle states in the transition of interrupt delivery are discarded if the interrupt is not successfully handled. In the case when the interrupt is disabled in the CPU but not masked in the IC, the states of IC fallback to their original value. This model is still valid in the sense that we can delay this state change of IC until the next time when the interrupt is raised again for that particular device and gets handled successfully.
 
3
Remember, we consider device drivers a part of the device, not the kernel.
 
Literature
1.
Alkassar, E.: OS verication extended: on the formal verication of device drivers and the correctness of client/server software. PhD thesis, Saarland University, Computer Science Department (2009)
2.
Alkassar, E., Hillebrand, M.A.: Formal functional verification of device drivers. In: Proceedings of the Verified Software: Theories, Tools, Experiments Second International Conference (VSTTE), Toronto, Canada, pp. 225–239 (2008)
3.
Alkassar, E., Cohen, E., Hillebrand, M., Pentchev, H.: Modular specification and verification of interprocess communication. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD Inc, Austin, TX, FMCAD ’10, pp. 167–174 (2010a)
4.
Alkassar, E., Paul, W., Starostin, A., Tsyban, A.: Pervasive verification of an OS microkernel: inline assembly, memory consumption, concurrent devices. In: Verified Software: Theories, Tools, Experiments (VSTTE 2010), Edinburgh, UK, pp. 71–85 (2010b)
5.
Amani, S., Chubb, P., Donaldson, A., Legg, A., Ryzhyk, L., Zhu, Y.: Automatic verification of message-based device drivers. In: Systems Software Verification, Sydney, Australia, pp. 1–14 (2012)
6.
Andronick, J., Lewis, C., Morgan, C.: Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: van Glabbeek RJ, Groote JF, Höfner P (eds) Workshop on models for formal analysis of real systems (MARS 2015), Suva, Fiji, pp. 10–24 (2015)
7.
Andronick, J., Lewis, C., Matichuk, D., Morgan, C., Rizkallah, C.: Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency, pp. 52–68. Springer, Berlin (2016)MATH
8.
Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, ACM, New York, NY, USA, EuroSys ’06, pp. 73–85 (2006)
9.
Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD Inc, Austin, TX, FMCAD ’10, pp. 35–42 (2010)
10.
11.
Chen, H., Wu, X.N., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible OS kernels and device drivers. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, New York, NY, USA, PLDI ’16, pp. 431–447 (2016)
12.
Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.: An empirical study of operating systems errors. In: Proceedings of the 18th ACM Symposium on Operating Systems Principles, ACM, New York, NY, USA, SOSP ’01, pp. 73–88 (2001)
13.
de Moura, L.M., Bjørner, N.: Z3: An efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), pp. 337–340 (2008)
14.
Duan, J.: Formal verification of device drivers in embedded systems. PhD thesis, University of Utah (2013)
15.
Duan, J., Regehr, J.: Correctness proofs for device drivers in embedded systems. In: Proceedings of the 5th International Conference on Systems Software Verification, USENIX Association, Berkeley, CA, USA, SSV’10, p. 5 (2010)
16.
Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: Proceedings of the ACM Conference on Programming Language Design and Implementation, pp. 170–182 (2008)
17.
Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. J. Autom. Reason. 42(2–4), 301–347 (2009)CrossRefMATH
18.
Ganapathi, A., Ganapathi, V., Patterson, D.: Windows XP kernel crash analysis. In: Proceedings of the 20th Conference on Large Installation System Administration, USENIX Association, Berkeley, CA, USA, LISA ’06, pp. 12–12 (2006)
19.
Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X., Weng, S.C., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: Proceedings of the 42nd ACM Symposium on Principles of Programming Languages, pp. 595–608 (2015)
20.
Gu, R., Shao, Z., Chen, H., Wu, X.N., Kim, J., Sjöberg, V., Costanzo, D.: Certikos: An extensible architecture for building certified concurrent os kernels. In: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, USENIX Association, Berkeley, CA, USA, OSDI’16, pp. 653–669 (2016)
21.
Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (2014)
22.
Intel: 82093AA I/O advanced programmable interrupt controller (I/O APIC) datasheet. Specification (1996)
23.
Intel: Multiprocessor specification, version 1.4. Specification (1997)
24.
Khoroshilov, A., Mutilin, V., Petrenko, A., Zakharov, V.: Establishing Linux driver verification process. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) Perspectives of Systems Informatics. Lecture Notes in Computer Science, vol. 5947, pp. 165–176. Springer, Berlin (2010)
25.
Kim, M., Choi, Y., Kim, Y., Kim, H.: Formal verification of a flash memory device driver - an experience report. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) Model Checking Software. Lecture Notes in Computer Science, vol. 5156, pp. 144–159. Springer, Berlin (2008)
26.
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP), Big Sky, MT, US, pp. 207–220 (2009)
27.
Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)CrossRef
28.
Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Proceedings of the Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2010), pp. 348–370 (2010)
29.
30.
Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformation. J. Autom. Reason. 41(1), 1–31 (2008)MathSciNetCrossRefMATH
31.
32.
Monniaux, D.: Verification of device drivers and intelligent controllers: a case study. In: Kirsch C, Wilhelm, R. (eds.) Proceedings of the 7th ACM International Conference On Embedded Software, EMSOFT 2007, pp. 30–36. ACM & IEEE (2007)
33.
O’Hearn, P.W.: Resources, concurrency and local reasoning. In: Proceedings of the 15th International Conference on Concurrency Theory (CONCUR’04), pp. 49–67 (2004)
34.
35.
Paulson, L.C.: Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828. Springer (1994)
36.
Pentchev, H.: Sound semantics of a high-level language with interprocessor interrupts. PhD thesis, Saarland University, Computer Science Department (2016)
37.
Ryzhyk, L., Chubb, P., Kuz, I., Le Sueur, E., Heiser, G.: Automatic device driver synthesis with Termite. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP), Big Sky, MT, US, pp. 73–86 (2009)
38.
Ryzhyk, L., Walker, A.C., Keys, J., Legg, A., Raghunath, A., Stumm, M., Vij, M.: User-guided device driver synthesis. In: USENIX Symposium on Operating Systems Design and Implementation, Broomfield, CO, USA, pp. 661–676 (2014)
39.
Schwarz, O., Dam, M.: Formal verification of secure user mode device execution with DMA. In: Yahav, E. (ed.) Hardware and Software: Verification and Testing, Lecture Notes in Computer Science, vol. 8855, pp. 236–251. Springer (2014)
40.
41.
Witkowski, T.: Formal verification of Linux device drivers. Master’s thesis, Dresden University of Technology (2007)
42.
Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of the 2010 ACM Conference on Programming Language Design and Implementation, pp. 99–110 (2010)
Metadata
Title
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
Authors
Hao Chen
Xiongnan Wu
Zhong Shao
Joshua Lockerman
Ronghui Gu
Publication date
23-12-2017
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 1-4/2018
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-017-9446-0

Other articles of this Issue 1-4/2018

Journal of Automated Reasoning 1-4/2018 Go to the issue

OriginalPaper

Distant Decimals of : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation

OriginalPaper

Verified iptables Firewall Analysis and Verification

EditorialNotes

Introduction to Milestones in Interactive Theorem Proving

OriginalPaper

Formally Verified Algorithms for Upper-Bounding State Space Diameters

OriginalPaper

Formalization of the Resolution Calculus for First-Order Logic

OriginalPaper

Regular Language Representations in the Constructive Type Theory of Coq

Premium Partner

    Image Credits