Mechanization of a noninterference proof for a toy imperative language with small-step semantics in Coq
-
Updated
Jun 3, 2026 - Rocq Prover
#
noninterference
Here are 5 public repositories matching this topic...
The Agda mechanization of a gradual security-typed programming language with general mutable references.
semantics agda formalization coercion meta-theory gradual-typing information-flow type-systems noninterference
-
Updated
Apr 5, 2025 - Agda
Strong non-interference for fine-grained concurrent programs
-
Updated
Mar 11, 2022 - Coq
Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby
-
Updated
Feb 14, 2018 - Coq
A capability-secure operating system derived from mathematical first principles — machine-checked noninterference proof in Z3, a full reference implementation, compile-time unforgeable capabilities in Rust, and a kernel that boots on bare metal enforcing its own proven guarantees.
rust computer-science security kernel x86-64 osdev operating-system z3 formal-methods microkernel smt-solver bare-metal formal-verification no-std systems-programming information-flow-control capability-security noninterference
-
Updated
Jul 11, 2026 - Python
Improve this page
Add a description, image, and links to the noninterference topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the noninterference topic, visit your repo's landing page and select "manage topics."