Security
Summarised papers
- Verifying constant-time implementations [almeida:security: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]
- 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]
- 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]
- 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]