Security

Summarised papers

Verifying constant-time implementations [almeida:security:2016]
Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor [becker:fm:2016]
End-to-end verification of information flow security for C and assembly programs [costanzo:pldi:2016]
SecChisel: Language and tool for practical and scalable security verification of security-aware hardware architectures [deng:hasp:2019]
Attacking, repairing, and verifying SecVisor: A retrospective on the security of a hypervisor [franklin:cmu:2008]
Secure autonomous cyber-physical systems through verifiable information flow control [liu:cpsspc:2018]
Verifying security invariants in ExpressOS [mai:asplos:2013]
seL4: from general purpose to a proof of information flow enforcement [murray:secpriv:2013]
Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
Noninterference, transitivity, and channel-control security policies [rushby:sri:1992]
SecVisor: A tiny hypervisor to provide lifetime kernel code integrity for commodity OSes [seshadri:sosp:2007]
StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities [skorstengaard:popl:2019]
Complete information flow tracking from the gates up [tiwari:asplos:2009]
überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]
A type system for expressive security policies [walker:popl:2000]
A hardware design language for timing-sensitive information flow security [zhang:asplos:2015]

Unsummarised papers

Hyperproperties [clarkson:jcs:2010]
The last mile: An empirical study of timing channels on seL4 [cock:ccs:2014]
A lattice model of secure information flow [denning:cacm:1976]
Verification of a practical hardware security architecture through static information flow analysis [ferraiuolo:asplos:2017]
HyperFlow: A processor architecture for nonmalleable, timing-safe information flow security [ferraiuolo:ccs:2018]
Secure information flow verification with mutable dependent types [ferraiuolo:dac:2017]
Security policies and security models [goguen:secpriv:1982]
Unwinding and inference control [goguen:secpriv:1984]
Ironclad apps: End-to-end security via automated full-system verification [hawblitzel:osdi:2014]
Testing noninterference, quickly [hritcu:icfp:2013]
Specifying and verifying hardware for tamper-resistant software [lie:secpri:2003]
Controlling the what and where of declassification in language-based security [mantel:pls:2007]
Enforcing robust declassification [myers:csfw:2004]
Virtualization: Issues, security threats, and solutions [pearce:compsurv:2013]
Declassification: Dimensions and principles [sabelfield:jcs:2009]
Execution leases: A hardware-supported mechanism for enforcing strong non-interference [tiwari:isca:2009]
Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security [tiwari:isca:2011]
Alias types for recursive data structures [walker:tic:2001]
Robust declassification [zdancewic:csfw:2001]
Observational determinism for concurrent program security [zdancewic:csfw:2003]