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
• scientific article; zbMATH DE number 1798185
• Completeness of a bytecode verifier and a certifying Java-to-JVM compiler
• Fundamental Approaches to Software Engineering
• scientific article; zbMATH DE number 1701360
• Improving the official specification of Java bytecode verification

Cites work

• scientific article; zbMATH DE number 2161330 (Why is no real title available?)
• 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
• Stack-based access control and secure information flow

Cited in

(7)

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

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)