Formalizing non-interference for a simple bytecode language in Coq

DOI10.1007/s00165-007-0055-2zbMath1151.68633OpenAlexW2156734947MaRDI QIDQ931434

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)

Related Items

Control and synthesis of non-interferent timed systems

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• A semantic approach to secure information flow
• Verified bytecode verifiers.
• A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
• Types, bytes, and separation logic
• Certification of programs for secure information flow
• Stack-based access control and secure information flow
• Fundamental Approaches to Software Engineering
• A formulation of the simple theory of types
• Verification, Model Checking, and Abstract Interpretation