Security types preserving compilation

DOI10.1016/j.cl.2005.05.002zbMath1109.68025OpenAlexW2017639917WikidataQ115098008 ScholiaQ115098008MaRDI QIDQ865705

Gilles Barthe, Tamara Rezk, Amitabh Basu

Publication date: 20 February 2007

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cl.2005.05.002

zbMATH Keywords

securityprogram analysisnon-interferencelow-level languages

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Related Items (3)

Unnamed Item ⋮ Unnamed Item ⋮ Output-sensitive information flow analysis

Uses Software

• Coq
• Isabelle/HOL
• JFlow
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Java bytecode verification: Algorithms and formalizations
• Isabelle/HOL. A proof assistant for higher-order logic
• Verified bytecode verifiers.
• Secrecy by typing in security protocols
• Modern Compiler Implementation in Java
• A uniform type structure for secure information flow
• Theoretical Computer Science
• Fundamental Approaches to Software Engineering
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Security types preserving compilation