[PL-reading-group] Verified OS papers

Joe Hallett jhallett at cs.bu.edu
Mon Sep 18 10:41:52 EDT 2006


Hi all,

Below are the links to the papers that we have collected for the reading 
group (thanks for everyone's help).  The first link is a paper that gives 
general motivation for a verified OS.  It's very short and has the feel of a 
survey article.  The rest of the links are divided by category.  It seems to 
me that the OS-design and kernel categories are the most closely related to 
our reading group.  The compiler category gives two papers about verifying 
the correctness of compilers.  The programming and proving environment 
papers discuss tools to accomplish this sort of verification.

I suggest that we meet this Friday to at least touch bases with each other. 
We can at least have an informal discussion about the "OS Verification - 
Now!" paper and if someone is willing we can present another paper.

I also suggest that we vote via email on the first three papers that we'd 
like to cover.  This way we can get an idea of where we are going with the 
reading group.  How does this sound?

My votes are (in no particular order):

"Running the Manual: An Approach to High-Assurance Mircokernel Development"
http://www.cse.unsw.edu.au/~chak/papers/sel4-model.pdf

"An Overview of the Singularity Project"
ftp://ftp.research.microsoft.com/pub/tr/TR-2005-135.pdf

"Formalising the L4 Microkernel API"
http://www.cse.unsw.edu.au/~kleing/papers/kolanski-klein-05.pdf

Joe

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

*motivation for a full-fledge verified OS :

"OS Verification - Now!"
http://www.ertos.nicta.com.au/publications/papers/Tuch_KH_05.pdf

*OS-design :

"An Overview of the Singularity Project"
ftp://ftp.research.microsoft.com/pub/tr/TR-2005-135.pdf

"Language Support for Fast and Reliable Message-based Communication in 
Singularity OS"
http://www.cs.kuleuven.ac.be/conference/EuroSys2006/papers/p177-fahndrich.pdf

"Luna: a Flexible Java Protection System"
www.cs.utah.edu/~wilson/compilers/old/papers/luna.ps

"A Principled Approach to Operating System Construction in Haskell"
http://www.cse.ogi.edu/~hallgren/ICFP2005/house.pdf

"Java Operating Systems: Design and Implementation"
http://www.cs.utah.edu/flux/papers/javaos-tr98015-abs.html

"Implementing Multiple Protection Domains in Java"
http://www.cs.cornell.edu/slk/papers/usenix98-final.pdf

"GrailOS: A micro-kernel based, multi-server, multi-personality operating 
system"
http://www.ertos.nicta.com.au/publications/papers/Leslie_06.pdf

K42/Tornado Operating System
http://www.eecg.toronto.edu/~tornado/

*kernel :

"Running the Manual: An Approach to High-Assurance Mircokernel Development"
http://www.cse.unsw.edu.au/~chak/papers/sel4-model.pdf

L4.Sec Microkernel Specification
http://os.inf.tu-dresden.de/L4/L4.Sec/

"Formalising the L4 Microkernel API"
http://www.cse.unsw.edu.au/~kleing/papers/kolanski-klein-05.pdf

"Formalising a High-Performance Microkernel"
http://ertos.nicta.com.au/publications/papers/Elphinstone_KK_06.pdf

and more:
http://ertos.nicta.com.au/research/l4.verified/pubs.pml

*network stack :

Network Semantics
http://www.cl.cam.ac.uk/~pes20/Netsem/

*programming :

The PoPLMark Challenge
http://fling-l.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=The_POPLmark_Challenge

Epigram: A dependently typed programming langauge
http://www.e-pig.org/

The Maude Sufficient Completeness Checker
http://maude.cs.uiuc.edu/tools/scc/

*proving environment :

The Isabelle theorem proving environment
http://isabelle.in.tum.de/

The HOL theorem proving environment
http://www.cl.cam.ac.uk/Research/HVG/HOL/

*compiler :

The Compcert certified compiler back-end
http://pauillac.inria.fr/~xleroy/compcert-backend/

A Verified Compiler in Isabelle/HOL
http://www.score.is.tsukuba.ac.jp/~okuma/vc/




More information about the PL-reading-group mailing list