CMU Theory of Secure Systems (ToSS) Project

• ToSS Home

Toss Project Related Work

This page is a repository for work related to the ToSS project at CMU.

• Formal Specification and Verification of Data Separation in a Separation Kernel for an Embedded System
  Constance Heitmeyer, Myla Archer, Elizabeth Leonard, and John McLean.
  Proceedings of 13th ACM Conference on Computer and Communication Security, Nov. 2006.
  


• Formalizing Information Flow in a Haskell Hypervisor
  Rebekah Leslie, Levent Erkok, and Flemming Andersen.
  


• Formal Pervasive Verification of a Paging Mechanism
  Eyad Alkassar, Norbert Schirmer, and Artem Starostin.
  Proceedings of TACAS 2008.
  


• On the verification of a "baby" hypervisor for a RISC machine; draft 0
  Eyad Alkassar and Wolfgang Paul.
  


• On the Correctness of Operating System Kernels
  Mauro Gargano, Mark Hillebrand, Dirk Leinenbach, and Wolfgang Paul.
  Proceedings of 18th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2005), Springer, LNCS 3603, pages 2-16, 2005.
  


• PSOS revisited
  P.G. Neumann and R.J. Feiertag.
  Proceedings of the 19th Annual Computer Security Applications Conference, 2003.
  


• Validating the Microsoft Hypervisor (Abstract)
  Ernie Cohen
  Invited Talk at Formal Methods: FM 2006.
  


• Secure microkernels, state monads and scalable refinement
  David Cock, Gerwin Klein and Thomas Sewell.
  TPHOLs '08, Montreal, Canada, August 2008.
  


• Nova Micro-Hypervisor Specification, Formal specification of the micro-hypervisor interface
  Hendrik Tews, Tjark Weber, Marcus Volp, Erik Poll, Marko van Eekelen, and Peter van Rossum.
  Radboud University Nijmegen, ICIS Technical Report ICIS-R08011, May 2008.
  


• Nova Micro-Hypervisor Verification, Formal, machine-checked verification of one module of the kernel source code
  Hendrik Tews, Tjark Weber, Marcus Volp, Erik Poll, Marko van Eekelen, and Peter van Rossum.
  Radboud University Nijmegen, ICIS Technical Report ICIS-R08012, May 2008.
  


• Verified protection model of the seL4 microkernel
  Dhammika Elkaduwe, Gerwin Klein and Kevin Elphinstone.
  Technical Report , NICTA, October, 2007.
  


• Towards trustworthy computing systems: taking microkernels to the next level
  Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters.
  ACM Operating Systems Review, 41(4), 3-11, (July, 2007)
  


• Towards a Practical, Verified Kernel
  Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe and Gernot Heiser.
  Proceedings of the 11th Workshop on Hot Topics in Operating Systems, San Diego, CA, USA, May, 2007.
  


• Formalising the L4 microkernel API
  Rafal Kolanski and Gerwin Klein.
  Computing: The Australasian Theory Symposium (CATS 06), Hobart, Australia, January, 2006.
  


• OS Verification -- Now!
  Harvey Tuch, Gerwin Klein, and Gernot Heiser.
  Proceedings HotOS X, Tenth Workshop on Hot Topics in Operating Systems, June 2005.