Mechanization of a noninterference proof for a toy imperative language with small-step semantics in Coq
-
Updated
Jun 3, 2026 - Rocq Prover
Mechanization of a noninterference proof for a toy imperative language with small-step semantics in Coq
The Agda mechanization of a gradual security-typed programming language with general mutable references.
Strong non-interference for fine-grained concurrent programs
A security-oriented programming language that enforces memory safety, information-flow, constant-time, and capability guarantees from one type discipline — with noninterference machine-checked in Lean 4.
Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby
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.
Detect undeclared cross-run communication channels in autonomous AI agent environments
To associate your repository with the noninterference topic, visit your repo's landing page and select "manage topics."