A verified information-flow architecture

DOI10.1145/2535838.2535839zbMath1284.68306arXiv1509.06503OpenAlexW2158763360MaRDI QIDQ5408414

Nathan A. Collins, Randy Pollack, Andrew Tolmach, David Pichardie, Delphine Demange, Cătălin Hriţcu, Arthur Azevedo de Amorim, Andre Dehon, Benjamin C. Pierce

Publication date: 10 April 2014

Published in: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1509.06503

zbMATH Keywords

securityformal verificationrefinementinformation-flow controlclean-slate designtagged architecture

Mathematics Subject Classification ID

Algorithmic information theory (Kolmogorov complexity, etc.) (68Q30) Semantics in the theory of computing (68Q55) Theory of operating systems (68N25)

Related Items (7)

CoSMed: a confidentiality-verified social media platform ⋮ Unnamed Item ⋮ Recycling proof patterns in Coq: case studies ⋮ Securing a compiler transformation ⋮ CoSMed: A Confidentiality-Verified Social Media Platform ⋮ Linear capabilities for fully abstract compilation of separation-logic-verified code ⋮ StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities

This page was built for publication: A verified information-flow architecture