A. Sabelfeld and A.C. Myers.
Language-Based Information-Flow Security.
In JSAC, 21(1), January 2003.
(PDF)
Z. Shao.
Certified Software.
In Communications of ACM, 53(12), December 2010.
(PDF)
L. Lamport. The Future of Computing: Logic or Biology
(PDF). July 2003.
P. Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing
(PDF). June 2000.
C.A.R. Hoare. Hints on Programming Language Design
(PDF). October 1973. Chapter 13 of the book on "Essays in Computing Science" by C.A.R. Hoare and C.B. Jones, available in the ACM digital library.
E.W.Dijkstra. Notes on Structured Programming
(PDF). January 1972. Chapter 1 of the book on "Structured Programming" by O.J.Dahl, E.W.Dijkstra, and C.A.R. Hoare, available in the ACM digital library.
X. Leroy, A. Appel, S. Blazy, and G. Stewart The CompCert Memory Model, Version 2.
(PDF)
X. Leroy and S. Blazy Formal verification of a C-like memory model and its uses for verifying program transformations.
(PDF)
S. Blazy and X. Leroy Mechanized semantics for the Clight subset of the C language.
(PDF)
Compiler Verification and CompCert
X. Leroy. Proving the Correctness of a Compiler.
Lecture Notes of EUTypes 2019 Summer School.
X. Leroy. The CompCert Verified Compiler
(html), Version 3.6, September 2019.
Certified Abstraction Layers
R. Gu, J. Koenig, T. Ramananandro, Z. Shao, N. Wu, S. Weng, H. Zhang, and Y. Guo. Deep Specifications and Certified Abstraction Layers.
In POPL'15.
(PDF)
A. Oliveira Vale, P.A. Mellies, Z. Shao, J. Koenig, L. Stefanesco. Layered and Object-Based Game Semanticss.
In POPL'22.
(PDF)
R. Gu, Z. Shao, J. Kim, N. Wu, J. Koenig, V. Sjoberg, H. Chen, D. Costanzo, and T. Ramananandro. Certified Concurrent Abstraction Layers.
In PLDI'18.
(PDF)
A. Oliveira Vale, Z. Shao, Y. Chen. A Compositional Theory of Linearizability.
In POPL'23.
(PDF)
R. Gu, Z. Shao, H. Chen, N. Wu, J. Kim, V. Sjoberg, and D. Costanzo. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.
In OSDI'16.
(PDF)
Information-Flow Security for mCertiKOS
D. Costanzo, Z. Shao, and R. Gu. End-to-End Verification of Information-Flow Security for C and Assembly Programs.
In PLDI'16.
(paper site)
Secure Remote Execution of Enclaves
P. Subramanyan, R. Sinha, I. Lebedev, S. Devadas, and S. Seshia. A Formal Foundation for Secure Remote Execution of Enclaves.
In CCS'17.
(PDF)
Smart Contract Security
M. Herlihy. Blockchains and Cryptocurrencies. Brown CS1951L, Spring 2019.
(course home page)
M. Herlihy. Atomic Cross-Chain Swaps.
In PODC'18.
(PDF)
M. Herlihy, B. Liskov, and L. Shrira. Cross-Chain Deals and Adversarial Commerce.
In VLDB'19.
(PDF)
HW Memory Model
S. Gerber, G. Zellweger, R. Achermann, K. Kourtis, T. Roscoe, and D. Milojicic. Not your parents' physical address space. In
HotOS'15. (PDF)
V. Costan and S. Devadas. Intel SGX Explained.
Sec 2.1,2.2,2.4,2.5, and 2.11. (PDF)
Virtual Machine Monitors (VMM)
G.J.Popek and R.P.Goldberg. Formal Requirements for
Virtualizable Third Generation Architectures. In CACM 17(7),
July 1974.
(PDF)
R.P.Goldberg. Survey of Virtual Machine Research. In IEEE Computer 7(9),
September 1974.
(PDF)
P. Barham et al. Xen and the Art of
Virtualization. SOSP'03 (PDF)
Microkernels
J. Liedtke. On Microkernel Construction.
In SOSP'95. (PDF)
J. Liedtke. Toward Real Microkernel.
In CACM 39(9), September 1996. (PDF)
G. Heiser. From L3 to seL4: What Have We Learnt in 20
Years of L4 Microkernels. In
SOSP'13. (PDF)
Capability-Based Systems
J.S. Shapiro et al. EROS: A Fast Capability System,
SOSP'99. (PDF)
H.M. Levy. Capability-Based Computer Systems,
Digital Press, 1984. Chapter 1
(PDF).
Here is the
link
for the entire book.
B. Frantz et al. GNOSIS: A Prototype Operating System
for the 1990's. (html). 1979.
Key Logic, Inc. KeyKOS - A Secure, High-Performance Environment for S/370. (html). SHARE 52 I, March 1988.
M.S. Miller et al. Capability Myths Demolished,
Technical Report SRL2003-02, Johns Hopkins University.
(PDF)
J.S.Shapiro and S. Weber. Verifying the EROS Confinement
Mechanism. IEEE Security&Privacy 2000.
(PDF)
seL4
G. Klein et al. Comprehensive Formal Verification of an
OS Microkernel. ACM TOCS 32(1), February 2014.
(PDF)
The seL4 open source site
and its reference manual
(PDF). August 2014.
T. Murray et al. seL4: from General Purpose to
a Proof of Information Flow Enforcement. IEEE Symp. on
Security and Privacy, May 2013.
(PDF)
T. Sewell et al. seL4 enforces integrity.
ITP 2011. (PDF)
DIFC-Based OS
N. Zeldovich et al.
Making Information Flow Explicit in HiStar.
In OSDI'06, November 2006.
(PDF)
P. Efstathopoulous et al.
Labels and Event Processes in the Asbestos Operating System. In SOSP'05, October 2005.
(PDF)
M. Krohn et al.
Information Flow Control for Standard OS Abstraction.
In SOSP'07, October 2007.
(PDF)
Coalgebra and Coinduction
J. Rutten Universal coalgebra: a theory of systems.
In Theoretical Computer Science 249 (2000) pages 3-80.
(PDF)
B. Jacobs and J. Rutten An Introduction to (co)algebra
and (co)induction. Chapter 2 of Advanced Topics in
Bisimulation and Coinduction edited by D. Sangiorgi and J. Rutten.
(PDF)
B. Jacobs Introduction to Coalgebra. Towards
Mathematics of States and Observations. Version 2.0, 2012.
(PDF)
S. Burris and H.P. Sankappanavar A Course in Universal Algebra.
(PDF)
Decentralized Information Flow Control
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)
A. Sabelfeld and D. Sands.
Declassification: Dimensions and Principles.
In Journal of Computer Security, 2007.
(PDF)
B. Lampson. A Note on the Confinement Problem.
In Communications of ACM, 16(10), October 1973.
(PDF)
Declassification and Noninterference
S. Chong and A.C. Myers.
End-to-End Enforcement of Erasure and Declassification.
In CSF'08. (PDF)
A. Sabelfeld and D. Sands.
Declassification: Dimensions and Principles.
In Journal of Computer Security, 2007.
(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)
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)
Exokernel and VMM Security
D.R. Engler et al. Exokernel: An Operating System Architecture
for Application-Level Resource Management, SOSP'95.
(PDF, slides)
T.Garfinkel et al. Terra: a Virtual Machine-Based Platform for
Trusted Computing, SOSP'03.
(PDF)
M.F. Kaashoek et al. Application Performance and Flexibility on
Exokernel Systems, SOSP'97.
(PDF)
Microkernels Meet Recursive Virtual Machines.
by Ford et al in OSDI'96
(PDF)
S. Hand et al. Are Virtual Machine Monitors Microkernels Done Right? In HotOS'05.
(html)
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)
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)
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.
Local Rely-Gurantee Reasoning.
In POPL'09,
January 2009. (PDF)
M. Fu et al.
Reasoning about Optimistic Concurrency Using a Program Logic for History.
In CONCUR'10,
September 2010. (PDF)