A Certified Lightweight Non-interference Java Bytecode Verifier

DOI10.1007/978-3-540-71316-6_10zbMath1187.68112OpenAlexW2102917576MaRDI QIDQ5756494

David Pichardie, Tamara Rezk, Gilles Barthe

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)

Related Items (8)

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 ⋮ A certified lightweight non-interference Java bytecode verifier ⋮ Specification and static enforcement of scheduler-independent noninterference in a middleweight Java ⋮ Verifying pointer and string analyses with region type systems ⋮ Relational bytecode correlations ⋮ Constructive Galois Connections

Uses Software

• Coq
• KRAKATOA

This page was built for publication: A Certified Lightweight Non-interference Java Bytecode Verifier