A Certified Lightweight Non-interference Java Bytecode Verifier

DOI10.1007/978-3-540-71316-6_10MaRDI QIDQ5756494zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, David Pichardie, Tamara Rezk

Publication date 4 September 2007

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-71316-6_10

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• A certified lightweight non-interference Java bytecode verifier
• Lightweight bytecode verification
• A type system for the Java bytecode language and verifier
• Noninterference with dynamic security domains and policies
• Verified bytecode verification and type-certifying compilation

Cited in

(14)

• Specification and static enforcement of scheduler-independent noninterference in a middleweight Java
• Verifying pointer and string analyses with region type systems
• Noninterference with dynamic security domains and policies
• Constructive Galois connections
• A certified lightweight non-interference Java bytecode verifier
• Fundamental Approaches to Software Engineering
• Theorem Proving in Higher Order Logics
• Hybrid information flow control for low-level code
• Information Flow Control-by-Construction for an Object-Oriented Language
• Symbolic abstract heaps for polymorphic information-flow guard inference
• Relational bytecode correlations
• Information Flow Noninterference via Slicing
• Inter-Procedural Information Flow Noninterference via Slicing
• Formalizing non-interference for a simple bytecode language in Coq

Describes a project that uses

Uses Software

• Coq
• KRAKATOA

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 Q5756494)