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

DOI10.1016/J.ENTCS.2020.08.005MaRDI QIDQ2229149zbMATH OpenOpenAlexWikidataFDO

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

zbMATH Keywords

Agdanon-interferencetype safetydependently-typed programminginformation flow type systems

Mathematics Subject Classification ID

Computer science (68-XX)

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

Cites work

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

Describes a project that uses

Uses Software

• Agda
• Haskell

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)