Mads Dam
ABSTRACT
A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a simple separation kernel for ARMv7. Previous work on information flow kernel security leaves communication to be handled by model-external means, and cannot be used to draw conclusions when there is explicit interaction between partitions. We propose a different approach where communication between partitions is made explicit and the information flow is analyzed in the presence of such a channel. Limiting the kernel functionality as much as meaningfully possible, we accomplish a detailed analysis and verification of the system, proving its correctness at the level of the ARMv7 assembly. As a sanity check we show how the security condition is reduced to noninterference in the special case where no communication takes place. The verification is done in HOL4 taking the Cambridge model of ARM as basis, transferring verification tasks on the actual assembly code to an adaptation of the BAP binary analysis tool developed at CMU.
- ARM TrustZone. http://www.arm.com/products/processors/technologies/trustzone.php.Google Scholar
- E. Alkassar, M. A. Hillebrand, W. J. Paul, and E. Petrova. Automated verification of a small hypervisor. In Proc. VSTTE, volume 6217 of Lecture Notes in Computer Science, pages 40--54. Springer, 2010. Google ScholarDigital Library
- ARMv7-A architecture reference manual. http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.ddi0406c.Google Scholar
- G. Barthe, G. Betarte, J. D. Campo, and C. Luna. Formally verifying isolation and availability in an idealized model of virtualization. In Proc. FM'11, volume 6664 of Lecture Notes in Computer Science, pages 231--245. Springer, 2011. Google ScholarDigital Library
- G. Barthe, G. Betarte, J. D. Campo, and C. Luna. Cache-leakage resilient os isolation in an idealized model of virtualization. In Proc. CSF'12, pages 186--197, Washington, DC, USA, 2012. IEEE Computer Society. Google ScholarDigital Library
- D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz. BAP: A binary analysis platform. In Proc. CAV'11, volume 6806 of Lecture Notes in Computer Science, pages 463--469. Springer, 2011. Google ScholarDigital Library
- A. C. J. Fox and M. O. Myreen. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In proc. ITP'10, volume 6172 of Lecture Notes in Computer Science, pages 243--258. Springer, 2010. Google ScholarDigital Library
- FreeRTOS. http://www.freertos.org/.Google Scholar
- V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In Proc. CAV'07, volume 4590 of Lecture Notes in Computer Science, pages 519--531. Springer, 2007. Google ScholarDigital Library
- C. Gehrmann, H. Douglas, and D. Nilsson. Are there good reasons for protecting mobile phones with hypervisors? In Consumer Communications and Networking Conference (CCNC), 2011 IEEE, pages 906 --911, jan. 2011.Google ScholarCross Ref
- J. A. Goguen and J. Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11--20, 1982.Google ScholarCross Ref
- C. Heitmeyer, M. Archer, E. Leonard, and J. McLean. Applying formal methods to a certifiably secure software system. IEEE Trans. Softw. Eng., 34(1):82--98, Jan. 2008. Google ScholarDigital Library
- HOL4. http://hol.sourceforge.net/.Google Scholar
- G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: formal verification of an OS kernel. In Proc. SOSP'09, pages 207--220. ACM, 2009. Google ScholarDigital Library
- P. C. Kocher. Timing attacks on implementations of Diffle-Hellman, RSA, DSS, and other systems. In Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, CRYPTO '96, pages 104--113, London, UK, 1996. Springer-Verlag. Google ScholarDigital Library
- D. Leinenbach and T. Santen. Verifying the Microsoft Hyper-V hypervisor with VCC. In Proc. FM'09, volume 5850 of Lecture Notes in Computer Science, pages 806--809. Springer Berlin Heidelberg, 2009. Google ScholarDigital Library
- J. McDermott, B. Montrose, M. Li, J. Kirby, and M. Kang. Separation virtual machine monitors. In Proceedings of the 28th Annual Computer Security Applications Conference, ACSAC '12, pages 419--428, New York, NY, USA, 2012. ACM. Google ScholarDigital Library
- uClinux. http://www.uclinux.org/.Google Scholar
- T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein. seL4: From general purpose to a proof of information flow enforcement. In IEEE Symposium on Security and Privacy, pages 415--429. IEEE Computer Society, 2013. Google ScholarDigital Library
- T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, and G. Klein. Noninterference for operating system kernels. In CPP, volume 7679 of Lecture Notes in Computer Science, pages 126--142. Springer, 2012. Google ScholarDigital Library
- Open Virtual Platforms. http://www.ovpworld.org/.Google Scholar
- W. J. Paul, S. Schmaltz, and A. Shadrin. Completing the automated verification of a small hypervisor - assembler code verification. In SEFM, volume 7504 of Lecture Notes in Computer Science, pages 188--202. Springer, 2012. Google ScholarDigital Library
- R. Richards. Modeling and security analysis of a commercial real-time operating system kernel. In D. S. Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applications, pages 301--322. Springer US, 2010.Google ScholarCross Ref
- J. Rushby. Noninterference, transitivity, and channel-control security policies. SRI International, Computer Science Laboratory, 1992.Google Scholar
- J. M. Rushby. Design and verification of secure systems. In Proc. SOSP'81, pages 12{21, 1981. Google ScholarDigital Library
- A. Sabelfeld and D. Sands. Declassification: Dimensions and principles. J. Comput. Secur., 17(5):517--548, Oct. 2009. Google ScholarCross Ref
- R. Sailer, E. Valdez, T. Jaeger, R. Perez, L. V. Doorn, J. L. Griffin, S. Berger, R. Sailer, E. Valdez, T. Jaeger, R. Perez, L. Doorn, J. Linwood, and G. S. Berger. sHype: Secure hypervisor approach to trusted virtualized systems. In IBM Research Report RC23511, 2005.Google Scholar
- D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2012. Google ScholarDigital Library
- T. A. L. Sewell, M. O. Myreen, and G. Klein. Translation validation for a verified os kernel. In Proc. PLDI'13, pages 471--482, 2013. Google ScholarDigital Library
- M. M. Wilding, D. A. Greve, R. J. Richards, and D. S. Hardin. Formal verification of partition management for the AAMP7G microprocessor. In Design and Verification of Microprocessor Systems for High-Assurance Applications, pages 175--191. Springer US, 2010.Google ScholarCross Ref
- Y. Zhang, A. Juels, M. K. Reiter, and T. Ristenpart. Cross-VM side channels and their use to extract private keys. In Proc. CCS'12, pages 305--316. ACM, 2012. Google ScholarDigital Library
Index Terms
- Formal verification of information flow security for a simple arm-based separation kernel
Recommendations
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Provably secure memory isolation for Linux on ARM
The isolation of security critical components from an untrusted OS allows to both protect applications and to harden the OS itself. Virtualization of the memory subsystem is a key component to provide such isolation. We present the design, implementation ...
Coverage metrics for formal verification
In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors of ...
Reviews
Prahladavaradan Sampath
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. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments