CS 528/428 Reading List, Spring 2009

Last modified: February 12, 2009.

Content

Background and Overview
Separation Logic and Hoare Logic
Certified Assembly Programming (CAP)
Concurrent Separation Logic (CSL)
CSL meets Rely-Guarantee
Singularity and OS Processes
Decentralized Information Flow Control (DIFC)
DIFC for Secure OS and Applications
Noninterference and Declassification
JavaScript and Web Applications
Context Logic
Event-Based Programming
Liveness Properties
Abstract Separation Logic
Certified Compiler and Translation Validation
Microkernels and Virtual Machines

Background and Overview

L. Lamport. The Future of Computing: Logic or Biology (PDF).

P. Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing (PDF).

F.B. Schneider, G. Morrisett, and R. Harper. A Language-Based Approach to Security (PDF).

M. Huth and M. Ryan. Logic in Computer Science: Modelling and Reasoning about Systems (Second Edition), Chapters 1-2, ISBN 052154310X (buy it online), Cambridge University Press, 2004.

G. Huet, G. Kahn and C. Paulin-Mohring. The Coq Proof Assistant: A Tutorial (Version 8.0) (HTML and PDF). April 27, 2004.

E. Gimenez and P. Casteran. A Tutorial on [Co-]Inductive Types in Coq (Version 8.0) (PDF). January 5, 2005.

D. Aspinall and T. Kleymann, User Manual for Proof General 3.5 (HTML and PDF). April 2004.

H. Barendregt and H. Geuvers. Proof-Assistants Using Dependent Type Systems. Download the reprint. Also in Handbook of Automated Reasoning (Volume 2), MIT Press, 2001.

Y. Bertot and P. Casteran. Interactive Theorem Proving and Program Development (Coq'Art: The Calculus of Inductive Constructions), ISBN 3540208542 (buy it online), Springer, 2004.

Separation Logic and Hoare Logic

J.C. Reynolds. An Introduction to Separation Logic. Lecture Notes for the FIRST PhD Fall School on Logics and Semantics of State, Copenhagen, October 2008. (PDF; also see an older version of the slides and a more recent version of the lecture notes)

C.A.R. Hoare. An axiomatic basis for computer programming, CACM 12(10), 1969, pages 576 - 580.

C.A.R. Hoare. Proof of a Program : FIND, CACM, 14(1), 1971, pages 39-45.

Certified Assembly Programming (CAP)

D. Yu, N.A. Hamid, and Z. Shao. Building Certified Library for PCC: Dynamic Storage Allocation. In Science of Computer Programming (Special Issue ESOP 2003), 50 (1-3): 101-127, March 2004. (PDF and coq-imp)

D. Yu and Z. Shao. Verification of Safety Properties for Concurrent Assembly Code. In ICFP'04, September 2004. (PDF and coq-imp)

Z. Ni and Z. Shao. Certified Assembly Programming with Embedded Code Pointers. In POPL'06, January 2006. (PDF and coq-imp)

Concurrent Separation Logic (CSL)

P.W. O'Hearn. Resources, Concurrency and Local Reasoning. In Theoretical Computer Science, 375 (1-3): 271-307, May 2007. (PDF; also see O'Hearn's slides in pdf)

R. Bornat, C. Calcagno, P.W. O'Hearn, and M. Parkinson. Permission Accounting in Separation Logic. In POPL'05, January 2005. (PDF; ; also see Bornat's slides in pdf)

M. Parkinson, R. Bornat, and P. O'Hearn. Modular Verification of a Non-Blocking Stack. In POPL'07, January 2007. (PDF)

X. Feng, Z. Shao, Y. Dong and Y. Guo. Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. In PLDI'08, June 208. (PDF)

CSL meets Rely-Guarantee

X. Feng. Local Rely-Gurantee Reasoning. In POPL'09, January 2009. (PDF)

V. Vafeiadis. Modular Fine-Grained Concurrency Verification. PhD dissertation. University of Cambridge, July 2008 (PDF, mainly Chapters 2-3 but Chapters 4-5 are interesting too). This is an expanded version of the RGSep CONCUR'07 paper by Vafeiadis and Parkinson)

X. Feng, R. Ferreira, and Z. Shao. On the Relationship between Concurrent Separation Logic and Assume-Guarantee Reasoning. In ESOP'07, April 2007. (PDF)

Singularity and OS Processes

G. Hunt, C. Hawblitzel, O. Hodson, J. Larus, B. Steensgaard, and T. Wobber. Sealing OS Processes to Improve Dependability and Safety. In EuroSys'07, March 2007 (PDF)

M. Fahndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. Hunt, J. R. Larus, and S. Levi. Language Support for Fast and Reliable Message-based Communication in Singularity OS. In EuroSys'06. April 2006 (PDF)

G. Back, W.C. Hsieh, and J. Lepreau. Processes in KaffeOS: Isolation, Resource Management, and Sharing in Java. In OSDI'00. October 2000. (PDF)

C. Hawblitzel and T. von Eicken. Luna: a Flexible Java Protection System. In OSDI'02. (HTML)

Decentralized Information Flow Control (DIFC)

A.C. Myers and B. Liskov. Protecting Privacy using Decentralized Label Model. In TOSEM'00, October 2000. (PDF)

A.C. Myers. JFlow: Practical Mostly-Static Information Flow Control.In POPL'99, January 1999. (PDF)

B. Lampson. A Note on the Confinement Problem. In Communications of ACM, 16(10), October 1973. (PDF)

A. Sabelfeld and A.C. Myers. Language-Based Information-Flow Security. In IEEE Journal on Selected Areas in Communications, 21(1), January 2003. (PDF)

DIFC for Secure OS and Applications

P. Efstathopoulous, M. Krohn, S. VanDeBogart, C. Frey, D. Ziegle, E. Kohler, D. Mazieres, F. Kaashoek, and R. Morris. Labels and Event Processes in the Asbestos Operating System. In SOSP'05, October 2005. (PDF)

N. Zeldovich, S. Boyd-Wickizer, E. Kohler, and D. Mazieres. Making Information Flow Explicit in HiStar. In OSDI'06, November 2006. (PDF)

M. Krohn, A. Yip, M. Brodsky, N. Cliffer, M.F. Kaashoek, E. Kohler, and R. Morris. Information Flow Control for Standard OS Abstraction. In SOSP'07, October 2007. (PDF)

N. Zeldovich, S. Boyd-Wickizer, and D. Mazieres. Securing Distributed Systems with Information Flow Control. In NSDI'08, April 2008. (PDF)

Noninterference and Declassification

M. Abadi, A. Banerjee, N. Heintze, and J.G. Riecke. A Core Calculus of Dependency. In POPL'99, January 1999. (PDF)

N. Heintze and J.G.Riecke. The SLam Calculus: Programming with Secrecy and Integrity. In POPL'98, January 1998. (PDF)

A.C. Myers, A. Sabelfeld, and S. Zdancewic. Enforcing Robust Declassification. In Journal of Computer Security, 14(2), 2006. (PDF)

P. Li and S. Zdancewic. Downgrading Policies and Relaxed Noninterference. In POPL'05, January 2005. (PDF)

A. Sabelfeld and D. Sands. Declassification: Dimensions and Principles. In Journal of Computer Security, 2007. (PDF)

S. Chong and A.C. Myers. End-to-End Enforcement of Erasure and Declassification. In CSF'08. (PDF)

D. Yu and N. Islam. A Typed Assembly Language for Confidentiality. In ESOP'06. April 2006. (PDF)

JavaScript and Web Applications

S. Chong, J. Liu, A.C. Myers, X. Qi, K. Vikram, L. Zheng, and X. Zheng. Secure Web Applications via Automatic Partitioning. In SOSP'07. October 2007. (PDF)

S. Chong, K. Vikram, and A.C. Myers. SIF: Enforcing Confidentiality and Integrity in Web Applications. In USENIX Security'07. (PDF)

H.J. Wang, X. Fan, C. Jackson, and J. Howell. Protection and Communication Abstractions for Web Browsers in MashupOS. In SOSP'07, October 2007. (PDF)

H.J. Wang, C. Grier, A. Moshchuk, S.T. King, P. Choudury, and H. Venter. The Multi-Principal OS Construction of the Gazelle Web Browser. Microsoft Technical Report MSR-TR-2009-16. February 2009. (PDF)

M.S. Miller, M. Samuel, B. Laurie, I. Awad, and M. Stay. Caja: Safe Active Content in Sanitized JavaScript. (Caja web site and PDF)

D. Yu, A. Chander, N.Islam, and I. Serikov. JavaScript Instrumentation for Browser Security. In POPL'07, January 2007. (PDF)

The Json web site.

Context Logic

C. Calcagno, P. Gardner, and U. Zarfaty. Context Logic and Tree Update. In POPL'05, January 2005. (PDF)

C. Calcagno, P. Gardner, and U. Zarfaty. Context Logic as Modal Logic: Completeness and Parametric Inexpressivity. In POPL'07, January 2007. (PDF)

P. Gardner, G.D. Smith, M.J. Wheelhouse, and U.D. Zarfaty. Local Hoare Reasoning about DOM. In PODS'08, June 2008. (PS)

Event-Based Programming

D. Gay, P. Levis, and D. Culler. Software Design Patterns for TinyOS. In ACM Transactions on Embedded Computing Systems, Vol. 6, No. 4, September 2007. (PDF)

D. Gay, P. Levis, R.V. Behren, M. Welsh, E. Brewer, and D. Culler. The nesC Language: A Holistic Approach to Networked Embedded Systems. In PLDI'03, June 2003. (PDF)

The TinyOS web site including extensive tutorials.

Liveness Properties

B. Cook. Principles of Program Termination Notes from the 2008 Marktoberdorf Summer School. (PDF)

B. Cook, A. Podelski, and A. Rybalchenko. Termination Proofs for Systems Code In PLDI'06, June 2006. (PDF)

A. Gotsman, B. Cook, M. Parkinson, and V. Vafeiadis. Proving that Non-blocking Algorithms Don't Block. In POPL'09, January 2009. (PDF)

B. Alpern and F. Schneider. Defining Liveness. In Information Processing Letters 21(4), October 1985. (PDF)

J. Berdine, A. Chawdhary, B. Cook, D. Distefano, and P. O'Hearn. Variance Analyses from Invariance Analyses. In POPL'07, January 2007. (PDF)

B. Cook, A. Gotsman, A. Podelski, A. Rybalchenko, and M.Y. Vardi. Proving that Programs Eventually Do Something Good. In POPL'07, January 2007. (PDF)

Abstract Separation Logic

C. Calcagno, P. O'Hearn, and H. Yang. Local Action and Abstract Separation Logic. In LICS'07, July 2007. (PDF)

M. Raza and P. Gardner. Footprints in Local Reasoning. Journal of Logical Methods in Computer Science (to appear), 2009. (PDF)

C.A.R. Hoare and P. O'Hearn. Separation Logic Semantics for Communicating Processes. In ENTCS 212, 2008. (PDF)

J. Brotherston and C. Calcagno. Classical BI (A Logic for Reasoning about Dualising Resources). In POPL'09, January 2009. (PDF)

Certified Compiler and Translation Validation

X. Leroy. Formal Certification of a Realistic Compiler.. In Communications of the ACM, April 2009 (PDF). An extended version of this paper can be found at here.

J.B. Tristan and X. Leroy. Formal Verification of Translation Validators: A Case Study on Instruction Scheduling Optimizations.. In POPL'08, January 2008. (PDF)

J.B. Tristan and X. Leroy. Verified Validation of Lazy Code Motion. In PLDI'09, June 2009. (PDF)

Microkernels and Virtual Machines

OSKit by Ford et al in SOSP'97

Microkernels Meet Recursive Virtual Machines by Ford et al in OSDI'96

Are Virtual Machine Monitors Microkernels Done Right? HotOS'05

Denali Isolation Kernel, OSDI'02

Xen and the Art of Virtualization, SOSP'03