A certified lightweight non-interference Java bytecode verifier

DOI10.1017/S0960129512000850MaRDI QIDQ5400855zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, David Pichardie, Tamara Rezk

Publication date 12 March 2014

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129512000850

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• A Certified Lightweight Non-interference Java Bytecode Verifier
• Java bytecode verification: Algorithms and formalizations
• Java bytecode verification: An overview
• Completeness of a bytecode verifier and a certifying Java-to-JVM compiler
• Fundamental Approaches to Software Engineering
• Verified bytecode verifiers
• Improving the official specification of Java bytecode verification

Cites work

• A Certified Lightweight Non-interference Java Bytecode Verifier
• A type system for the Java bytecode language and verifier
• Bytecode verification on Java smart cards
• Lightweight bytecode verification
• Principles of program analysis.
• Stack-based access control and secure information flow

Cited in

(7)

• Specification and static enforcement of scheduler-independent noninterference in a middleweight Java
• Noninterference with dynamic security domains and policies
• Fundamental Approaches to Software Engineering
• Theorem Proving in Higher Order Logics
• A Certified Lightweight Non-interference Java Bytecode Verifier
• Relational bytecode correlations
• Formalizing non-interference for a simple bytecode language in Coq

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A certified lightweight non-interference Java bytecode verifier

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