Formalizing non-interference for a simple bytecode language in Coq

DOI10.1007/S00165-007-0055-2MaRDI QIDQ931434zbMATH OpenOpenAlexWikidataFDO

Authors Florian Kammüller

Publication date 25 June 2008

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00165-007-0055-2

zbMATH Keywords

Formal methods for securityInteractive theorem provingModular specificationProgramming language analysis

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of software (68N99)

Recommendations

• A Certified Lightweight Non-interference Java Bytecode Verifier
• Formal verification of language-based concurrent noninterference
• A certified lightweight non-interference Java bytecode verifier
• Fundamental Approaches to Software Engineering
• Java bytecode verification: Algorithms and formalizations

Cites work

• scientific article; zbMATH DE number 1650458 (Why is no real title available?)
• scientific article; zbMATH DE number 53088 (Why is no real title available?)
• scientific article; zbMATH DE number 3584897 (Why is no real title available?)
• scientific article; zbMATH DE number 1418328 (Why is no real title available?)
• scientific article; zbMATH DE number 4189687 (Why is no real title available?)
• A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
• A formulation of the simple theory of types
• A semantic approach to secure information flow
• Certification of programs for secure information flow
• Fundamental Approaches to Software Engineering
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Java bytecode verification: Algorithms and formalizations
• Stack-based access control and secure information flow
• Types, bytes, and separation logic
• Verification, Model Checking, and Abstract Interpretation
• Verified bytecode verifiers.

Cited in

(5)

• Formalisation and implementation of an algorithm for bytecode verification of \(\@\)NonNull types
• Are there interactive protocols for co-NP languages?
• Relational bytecode correlations
• Control and synthesis of non-interferent timed systems
• Formal verification of language-based concurrent noninterference

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Formalizing non-interference for a simple bytecode language in Coq

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