CS 528/428 Reading List, Spring 2011
CS 528/428 Reading List, Spring 2011
Last modified: April 13, 2011. This page is still
under construction!
N. Falliere, L. Murchu, and E. Chien. W32.Stuxnet
Dossier PDF ).
F.B. Schneider, G. Morrisett, and R. Harper. A Language-Based Approach to Security PDF ).
A. Sabelfeld and A.C. Myers.
Language-Based Information-Flow Security PDF )
Z. Shao.
Certified Software PDF )
L. Lamport. The Future of Computing: Logic or Biology PDF ).
P. Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing PDF ).
R.P.Goldberg. Architecture of Virtual Machines PDF )
G.J.Popek and R.P.Goldberg. Formal Requirements for
Virtualizable Third Generation Architectures PDF )
J. Liedtke. On Microkernel Construction PDF )
Microkernels Meet Recursive Virtual Machines PDF )
P. Barham et al. Xen and the Art of
Virtualization PDF )
Whitaker et al. Scale and Performance in the Denali Isolation
Kernel html )
J.E. Smith and R. Nair. Virtual Machines google
book page )
S. Hand et al. Are Virtual Machine Monitors Microkernels Done Right? html )
D.R. Engler et al. Exokernel: An Operating System Architecture
for Application-Level Resource Management PDF , slides )
T.Garfinkel et al. Terra: a Virtual Machine-Based Platform for
Trusted Computing PDF )
M.F. Kaashoek et al. Application Performance and Flexibility on
Exokernel Systems PDF )
S. King et al. SubVirt: Implementing Malware with Virtual
Machines PDF )
D. Wentzlaff. An Operating System for Multicore and Clouds:
Mechanisms and Implementation PDF )
H.M. Levy. Capability-Based Computer Systems PDF )
M.S. Miller et al. Capability Myths Demolished PDF )
A.C. Bomberger et al. The KeyKOS NanoKernel
Architecture PDF )
J.S. Shapiro et al. EROS: A Fast Capability System PDF )
J.S.Shapiro and N. Hardy. EROS: A Principle-Driven Operating
System from the Ground Up PDF )
Documents available at the
KeyKos home page.
Documents available at the
EROS home page.
R.J. Lipton and L. Snyder. A Linear Time Algorithm for Deciding Subject Security PDF )
D. Elkaduwe et al. Verified Protection Model of the seL4 Microkernel PDF )
A. Boyton. A Verified Shared Capability Model PDF )
J.S.Shapiro. The Practical Application of a Decidable Access Model PDF )
J.S.Shapiro and S. Weber. Verifying the EROS Confinement
Mechanism PDF )
M. Hohmuth et al. Reducing TCB size by using untrusted
components: small kernels vesus virtual machine monitors PDF )
J.S.Shapiro et al. Towards a Verified General-Purpose Operating
System Kernel HTML )
A.C. Myers and B. Liskov.
Protecting Privacy using Decentralized Label Model PDF )
A.C. Myers.
JFlow: Practical Mostly-Static Information Flow Control PDF )
A. Sabelfeld and D. Sands.
Declassification: Dimensions and Principles PDF )
B. Lampson. A Note on the Confinement Problem PDF )
M. Krohn et al.
Information Flow Control for Standard OS Abstraction PDF )
M. Krohn and E. Tromer.
Noninterference for a Practical DIFC-Based Operating
System PDF )
P. Efstathopoulous et al.
Labels and Event Processes in the Asbestos Operating System PDF )
N. Zeldovich et al.
Making Information Flow Explicit in HiStar PDF )
N. Zeldovich et al.
Hardware Enforcement of Application Security Policies Using Tagged Memory PDF )
Indrajit Roy et al.
Laminar: Practical Fine-Grained Decentralized Information Flow
Control PDF )
W.R. Harris et al.
DIFC Programs by Automoatic Instrumentation PDF )
N. Zeldovich et al.
Securing Distributed Systems with Information Flow
Control PDF )
W.R. Harris et al.
Verifying Information Flow Control over Unbounded
Processes PDF )
A. Yip et al.
Improving Application Security with Data Flow Assertions PDF )
S. Chong and A.C. Myers.
End-to-End Enforcement of Erasure and Declassification PDF )
A. Sabelfeld and D. Sands.
Declassification: Dimensions and Principles PDF )
A.C. Myers, A. Sabelfeld, and S. Zdancewic.
Enforcing Robust Declassification PDF )
P. Li and S. Zdancewic.
Downgrading Policies and Relaxed Noninterference PDF )
M. Abadi, A. Banerjee, N. Heintze, and J.G. Riecke.
A Core Calculus of Dependency PDF )
N. Heintze and J.G.Riecke.
The SLam Calculus: Programming with Secrecy and Integrity PDF )
J.C. Reynolds. An Introduction to Separation Logic PDF ; also
see an
older version of the slides
and
a more recent version of the lecture notes)
P.W. O'Hearn.
Resources, Concurrency and Local Reasoning Theoretical Computer Science ,
375 (1-3): 271-307, May 2007. (PDF ; also see O'Hearn's slides in pdf )
V. Vafeiadis. Modular Fine-Grained Concurrency
Verification 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.
Local Rely-Gurantee Reasoning POPL'09 ,
January 2009. (PDF )
M. Fu et al.
Reasoning about Optimistic Concurrency Using a Program Logic for History CONCUR'10 ,
September 2010. (PDF )
I. Filipovic et al.
Abstraction for Concurrent Objects PDF )
A. Turon and M. Wand.
A separation logic for refining concurrent objects PDF )
M.P.Herlihy and J.M.Wing.
Linearizability: A Correctness Condition for Concurrent Objects PDF )
E. Love et al.
Enhancing Security via Provably Trustworthy Hardware Intellectual Property PDF )
L. Strozek.
Verilog Tutorial PDF )
M. Bickford and R.L. Constable.
A Causal Logic of Events in Formalized Computational Type Theory PDF )
M. Bickford and R.L. Constable.
Automated Proof of Authentication Protocols in a Logic of
Events PDF )
H.J. Wang, X. Fan, C. Jackson, and J. Howell.
Protection and Communication Abstractions
for Web Browsers in MashupOS PDF )
J. Magazinius et al.
A Lattice-based Approach to Mashup Security 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 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 PDF )
The Json web site.
M. Dodds et al.
Modular reasoning for deterministic parallelism PDF )
M. Dodds et al.
Deny-Guarantee Reasoning PDF )
Copyright (c) 2009-2011,
Zhong Shao ,
Dept. of Computer Science ,
Yale University.