Security types preserving compilation

DOI10.1016/J.CL.2005.05.002MaRDI QIDQ865705zbMATH OpenOpenAlexWikidataFDO

Authors 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

low-level languagesnon-interferenceprogram analysissecurity

Mathematics Subject Classification ID

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

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• Programming Languages and Systems
• More Typed Assembly Languages for Confidentiality
• Secure information flow via linear continuations
• scientific article; zbMATH DE number 1692933

Cites work

• A uniform type structure for secure information flow
• Fundamental Approaches to Software Engineering
• scientific article; zbMATH DE number 1692933 (Why is no real title available?)
• scientific article; zbMATH DE number 1696586 (Why is no real title available?)
• scientific article; zbMATH DE number 1956459 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• Java bytecode verification: Algorithms and formalizations
• Modern Compiler Implementation in Java
• Secrecy by typing in security protocols
• Theoretical Computer Science
• Verification, Model Checking, and Abstract Interpretation
• Verified bytecode verifiers.

Cited in

(16)

• Secure information flow via linear continuations
• scientific article; zbMATH DE number 1692933 (Why is no real title available?)
• A secure compiler for ML modules
• scientific article; zbMATH DE number 1948407 (Why is no real title available?)
• On flow-sensitive security types
• Theoretical Computer Science
• Theoretical Aspects of Computing – ICTAC 2005
• Output-sensitive information flow analysis
• scientific article; zbMATH DE number 7649976 (Why is no real title available?)
• Programming Languages and Systems
• Verification, Model Checking, and Abstract Interpretation
• Securing a compiler transformation
• Securing a compiler transformation
• Hybrid information flow control for low-level code
• Output-sensitive information flow analysis
• Integration of a security type system into a program logic

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• JFlow
• TALx86

This page was built for publication: Security types preserving compilation

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