Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Formal verification of information flow security for a simple ARM-based separation kernel
Dam M., Guanciale R., Khakpour N., Nemati H., Schwarz O.  CCS 2013 (Proceedings of the 2013 ACM SIGSAC Conference on Computer & Communications Security, Berlin, Germany, Nov 4-8, 2013)223-234.2013.Type:Proceedings
Date Reviewed: Jan 27 2014

There has been considerable recent interest in verifying operating systems [1,2]. One of the difficulties with this form of software verification is simply stating the verification problem formally and succinctly. This, combined with the fact that some of the critical parts of an operating system depend on services provided by a processor and programmed in assembly language, makes the task even more daunting.

This paper presents the verification of a separation kernel, which provides a “Chinese wall” between two virtual machines. The specification of such a kernel is formulated as a set of operational semantic rules. This specification can be seen to be “correct by construction” with respect to the Chinese-wall properties that a separation kernel ought to satisfy. The authors construct a refinement relation between this ideal machine and the real kernel implemented in ARM assembly language.

One of the highlights of the paper is the use of a formalization of the ARM instruction set architecture within the HOL4 higher-order logic system. This allows expression of both the ideal and real kernel in the same platform, and enables the construction and verification of a bisimulation relation between the two. The authors have tried to achieve a high degree of automation in the verification effort by, for example, building custom tools to iterate through the ARM instruction set and proving clauses of the bisimulation relation in HOL4. The use of tools for the automatic construction of pre-post condition pairs for the interrupt handler and bootstrap code from the ideal specification is also quite ingenious.

Reviewer:  Prahladavaradan Sampath Review #: CR141933 (1405-0368)
1) Klein, G. et al. seL4: formal verification of an operating-system kernel. Communications of the ACM 53, 6(2010), 107–115.
2) Beckert, B.; Moskal, M. Deductive verification of system software in the Verisoft XT project. KI - Künstliche Intelligenz 24, 1(2010), 57–61.
Bookmark and Share
  Editor Recommended
 
 
Verification (D.4.6 ... )
 
 
Formal Methods (D.2.4 ... )
 
 
Software/ Program Verification (D.2.4 )
 
Would you recommend this review?
yes
no
Other reviews under "Verification": Date
Muse--a computer assisted verification system
Halpern J., Owre S., Proctor N., Wilson W. IEEE Transactions on Software Engineering SE-13(2): 151-156, 1987. Type: Article
Dec 1 1987
The Specification and Modeling of Computer Security
McLean J. Computer 23(1): 9-16, 1990. Type: Article
Oct 1 1990
Digital system verification: a combined formal methods and simulation framework
Li L., Thornton M., Morgan and Claypool Publishers, San Rafael, CA, 2010.  100, Type: Book (978-1-608451-78-4)
Oct 24 2011
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy