Running the manual: an approach to high-assurance microkernel development

No abstract is available for this paper.

• Publication year

  2006

• Venue

  ACM SIGPLAN Symposium/Workshop on Haskell

• Publication date

  2006-09-17

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1159842.1159850
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Fast and loose reasoning is morally correct

  2006cited by this paper
• Formalising the L4 microkernel API

  2006cited by this paper
• The VFiasco approach for a verified operating system

  2005influential reference
• OS Verification - Now!

  2005cited by this paper
• On the Correctness of Operating System Kernels

  2005cited by this paper
• Axiomatic Constructor Classes in Isabelle/HOLCF

  2005cited by this paper
• Verifying haskell programs using constructive type theory

  2005cited by this paper
• A principled approach to operating system construction in Haskell

  2005influential reference
• A Unified Memory Model for Pointers

  2005cited by this paper
• The logic of demand in Haskell

  2005cited by this paper
• Towards verified virtual memory in L4

  2004cited by this paper
• An Overview of the Programatica Toolset

  2004cited by this paper
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic

  2002cited by this paper
• Modeling and Verification of the RUBIS μ−Kernel with SPIN

  2002cited by this paper
• Isabelle/HOL: A Proof Assistant for Higher-Order Logic

  2002influential reference
• Interface and execution models in the Fluke kernel

  1999cited by this paper
• Toward real microkernels

  1996cited by this paper
• Lambdas in the liftshaft—functional programming and an embedded architecture

  1995cited by this paper
• Address space sparsity and fine granularity

  1994cited by this paper
• Modelization and verification of a multiprocessor realtime OS kernel

  1994cited by this paper
• Kit: A Study in Operating System Verification

  1989cited by this paper
• Message-Based Functional Operating Systems

  1986cited by this paper
• The transfer of information and authority in a protection system

  1979cited by this paper
• Specification and verification of the UCLA Unix security kernel

  1979cited by this paper
• The foundations of a provably secure operating system (PSOS)

  1979influential reference
• A Linear Time Algorithm for Deciding Subject Security

  1977cited by this paper
• Policy/mechanism separation in Hydra

  1975cited by this paper

• Property-Based Testing: Climbing the Stairway to Verification

  2022cites this paper
• Secure Memory Management on Modern Hardware

  2020cites this paper
• A Least-Privilege Memory Protection Model for Modern Hardware

  2019cites this paper
• An Overview of the Verification of the seL 4 Microkernel

  2018cites this paper
• Formal Verification of a Modern Boot Loader

  2018cites this paper
• Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)

  2018cites this paper
• Total Haskell is reasonable Coq

  2017influential citation
• Pip, un proto-noyau fait pour renforcer la sécurité dans les objets connectés

  2017cites this paper
• A blind processing framework to facilitate openness in smart grid communications

  2015cites this paper
• Leakage in Trustworthy Systems

  2014cites this paper
• Comprehensive formal verification of an OS microkernel

  2014cites this paper
• xmonad in Coq (experience report): programming a window manager in a proof assistant

  2013cites this paper
• Chapter 1 Trustworthy Real-Time Systems

  2012cites this paper
• Trustworthy Real-Time Systems

  2012cites this paper
• Large-scale formal verification in practice: A process perspective

  2012cites this paper
• Verification of programs in virtual memory using separation logic

  2011cites this paper
• Measures to improve security in a microkernel operating system

  2011cites this paper
• Enhancing data privacy and integrity in the cloud

  2011cites this paper
• Secure communications in the smart grid

  2011cites this paper
• A functional approach to memory-safe operating systems

  2011cites this paper
• Lyrebird - Assigning Meanings to Machines

  2010cites this paper
• Blind processing: Securing data against system administrators

  2010cites this paper
• Specifying and building a formal secure Virtual Monitor Machine prototype

  2010cites this paper
• Executing Petri net based system model

  2010cites this paper
• What Functional Programming Can Do for FreeBSD and Vice Versa

  2010cites this paper
• seL4: formal verification of an OS kernel

  2009cites this paper
• seL4: Formal Verification of an OS Kernel

  2009cites this paper
• Operating system verification—An overview

  2009cites this paper
• Experience report: seL4: formally verifying a high-performance microkernel

  2009influential citation
• Mind the Gap A Verification Framework for Low-Level C

  2009cites this paper
• A Verified Shared Capability Model

  2009cites this paper
• 5th International Verification Workshop - VERIFY'08

  2008cites this paper
• Verified Protection Model of the seL4 Microkernel

  2008cites this paper
• Bitfields and Tagged Unions in C: Verification through Automatic Generation

  2008cites this paper
• Mapped Separation Logic

  2008cites this paper
• Lightweight monadic regions

  2008cites this paper
• Kernel design for isolation and assurance of physical memory

  2008cites this paper
• Secure Microkernels, State Monads and Scalable Refinement

  2008cites this paper
• Beauty in the beast

  2007cites this paper
• Hype and Virtue

  2007cites this paper
• A memory allocation model for an embedded microkernel

  2007cites this paper
• Towards a Practical, Verified Kernel

  2007cites this paper
• Formalizing Information Flow in a Haskell Hypervisor

  2007cites this paper
• Kernel Development for High Assurance

  2007cites this paper
• Position : Lightweight static resources ? Sexy types for embedded and systems programming

  2007cites this paper
• Towards trustworthy computing systems: taking microkernels to the next level

  2007cites this paper
• Delimited Continuations in Operating Systems

  2007cites this paper
• First International Workshop on Microkernels for Embedded Systems

  2007cites this paper
• A Functional Semantics for the Awkward Squad

  2007cites this paper
• High-performance microkernels and virtualisation on ARM and segmented architectures

  2007cites this paper
• Beauty in the Beast A Functional Semantics for the Awkward Squad

  2007cites this paper