noninterference

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

Research specification for confidentiality-labelled information flow in type systems, with explicit audited declassification and declassification-aware noninterference as the proof target. Specification-stage only; no checker or runtime.

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.

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.

Formalisation of "Noninterference, Transitivity, and Channel-Control Security Policies" by J. Rushby

Detect undeclared cross-run communication channels in autonomous AI agent environments