Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types

DOI10.1016/J.ENTCS.2020.08.005OpenAlexW3092413010WikidataQ113317317 ScholiaQ113317317MaRDI QIDQ2229149FDOQ2229149

Authors: Cecilia Manzino, Alberto Pardo 

Publication date: 22 February 2021

Full work available at URL: https://doi.org/10.1016/j.entcs.2020.08.005

Recommendations

• On flow-sensitive security types
• Verification, Model Checking, and Abstract Interpretation
• Fundamentals of Computation Theory
• Cryptographically sound implementations for typed information-flow security
• Formalizing CCS and \(\pi\)-calculus in Guarded Cubical Agda
• Automated type-based analysis of injective agreement in the presence of compromised principals
• A security flow control algorithm and its denotational semantics correctness proof
• A type inference algorithm for secure ambients
• ZB 2005: Formal Specification and Development in Z and B

zbMATH Keywords

Agdanon-interferencetype safetydependently-typed programminginformation flow type systems

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Dependently typed programming in Agda
• Dependent Types at Work
• Concrete semantics. With Isabelle/HOL
• A lattice model of secure information flow
• On flow-sensitive security types
• From exponential to polynomial-time security typing via principal types

Uses Software

• Haskell
• Agda

This page was built for publication: Agda formalization of a security-preserving translation from flow-sensitive to flow-insensitive security types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2229149)