Mechanization of a noninterference proof via a type system for a simple imperative language with a small-step semantics in Coq.

Author: Aslan Askarov

• Rocq Prover version: 9.2 (the proof also builds with the coqc-compatible toolchain of recent Coq/Rocq releases).
• An (in-progress) description of the [proof architecture](#Proof Architecture) is below.
• The standard TINI theorem is at the bottom of NI.v.
• The workhorse noninterference reasoning is in NIBridge.v.

Usage

Build everything with dune:

dune build

Artifacts go to _build/ (the source tree stays clean). For interactive editing, VsCoq2 picks up the dune project automatically; for Proof General run dune build first (.dir-locals.el points it at _build/default).

Notes

• The proof scripts use CPDT tactics; they are included in lib/cpdt.
• The proof uses LibTactics and software foundation tactics SfLib.v; these and other small libraries are included for convenience in lib/.
• Comments and suggestions on how to improve these scripts are welcome.
• For a version of this proof technique applied to a dynamic monitor, see this repository https://github.com/Crowton/DynamicNoninterference

---

Proof Architecture

A more thorough description of the proof technique, including some introduction and background, is available in infoflow-basics.pdf.

The language and the semantics.

Our language is the standard imperative language, given by the following grammar

e := n | x | e + e
c := skip | x := e | c; c | if e then c else c | while e do c | stop

Semantics

Memory is a partial function from variable names to values. Variable x has value v in memory m, when m x = Some v.

Semantics is a mixed-step semantics. For expressions, we use a big-step evaluation relation eval m e v that means expression e evaluates to value v in memory m. Semantics for commands is given as a relation step cfg cfg', also written as cfg ⇒ cfg' that relates two configurations. A configuration is a pair of a command and a memory, often expressed using notation 〈c,m〉.

Reachability in zero or many steps, denoted as cfg ⇒* cfg', is defined later in module Bridge.v. The same module also defines reachability in at most n steps with the corresponding notation cfg ⇒/+ n +/ cfg'.

Security environment

We assume two security levels Low and High that form a simple two-point lattice, with a flowsto relation ⊑, such that for all ℓ we have ℓ ⊑ ℓ, and Low ⊑ High, but not High ⊑ Low.

A security environment is a partial function Γ mapping variable names to security levels. Variable x has security level ℓ in Γ when Γ x = Some ℓ.

Well-formedness

A memory m is well formed w.r.t. a security environment Γ when dom (m) = dom (Γ); this is formalized as wf_mem m Γ.

Low-equivalence

Two memories m and s are low-equivalent w.r.t. an environment Γ, when they each are well-formed w.r.t. Γ and they agree on the values of all low variables. This is denoted using relation state_low_eq Γ m s. Low-equivalence is formally defined in the module LowEq.v.

Type system

The type system is a standard information flow type system, in the style of Volpano Smith Irvine, aka Denning-style enforcement. Notation -{ Γ, pc ⊢ c}- means that program c is well-typed in the security environment Γ given the program counter label pc. The typing rules are standard, and are formalized in the module Types.v.

Preservation

The preservation theorem is standard. The following statement of the preservation theorem is an excerpt from WellFormedness.v.

Theorem preservation:
  forall Γ c m c' m' pc,
  -{ Γ, pc ⊢ c}- ->
 〈c, m 〉 ⇒ 〈c', m' 〉->
  wf_mem m Γ ->
  wf_mem m' Γ /\ ( c' <> STOP -> -{Γ, pc ⊢ c'}- ).

Noninterference

Top-level noninterference is the standard termination-insensitive noninterference. To prove NI we extend our semantics with with so-called events — the resulting event semantics is an augmentation of the original semantics. We also introduce bridge steps, that are the key tool in the proof. We show that each of these extensions is adequate w.r.t. the original small-step transition relation in the module Adequacy.v.

Event semantics

We distinguish between two kinds of events: low assignments, and empty events that correspond to all other steps. Events are propagated through sequential composition.

We say that an event step is a low step if it produces a low event, and is a high step otherwise.

The event semantics is defined in the module Augmented.v.

Bridge relation

Bridge relation is the key workhorse relation. Say that configuration cfg bridges to configuration cfg' when cfg' is the first configuration reachable from cfg after a low assignment or a cfg' is a terminal configuration. Bridge relation is defined in terms of the event semantics. Bridge relations are indexed by the number of intermediate steps, which is needed in order to apply the strong induction principle in the noninterference for bridge steps.

We use notation cfg ↷(Γ, ev, n) cfg' to denote that configuration cfg "bridges" to configuration cfg' producing event ev with n intermediate high steps. The following rules provide the idea behind the bridge relation; see the formal definition in the module Bridge.v for details.

low_event_step Γ ℓ evt cfg cfg'
____________________________________  [bridge_low_num]
cfg ↷(Γ, evt, 0) cfg'



high_event_step Γ ℓ evt cfg 〈STOP,m〉
____________________________________  [bridge_stop_num]
cfg ↷(Γ, evt, 0) 〈STOP,m〉



high_event_step Γ ℓ evt cfg cfg'
is_not_stop cfg'  
cfg' ↷(Γ, evt'', n) cfg''
____________________________________  [bridge_trans_num]
cfg ↷(Γ, evt'', n+1) cfg''

Noninterference for bridge steps.

The following is an excerpt from NIBridge.v, where the last four lines in the definition encode the postconditions.

Definition NI_idx (n: nat): Prop :=
  forall Γ pc c,
  -{ Γ, pc ⊢ c }- ->
  forall m s ev1 ev2 c2 d2 m2 s2 n',
    state_low_eq Γ m s ->
    〈c, m〉 ↷ ( Γ, ev1, n ) 〈c2, m2〉->
    〈c, s〉 ↷ ( Γ, ev2, n') 〈d2, s2〉->      
          state_low_eq Γ m2 s2 /\
          c2 = d2 /\
          (low_event Γ Low ev1 <-> low_event Γ Low ev2) /\
          (low_event Γ Low ev1 -> ev1 = ev2).

Theorem ni_bridge_num:
    forall n, NI_idx (n).

This theorem is proved using an outer strong induction on n, with inner inductions on the typing derivation. In the outer base case (n = 0) the only possible cases are skip, assignment, and sequential composition. In the outer inductive case the only possibly cases are sequential composition, if, and while commands.

Adequacy and relating to standard NI

We relate noninterference for the bridge relation to standard noninterference via adequacy of the bridge relation. The final connection is made in the module NI.v.

(** Standard termination-insensitive noninterference *)

Theorem TINI:
  forall Γ c m s m_end s_end pc,
    -{ Γ, pc ⊢ c }- ->
      state_low_eq Γ m s ->
        〈c, m 〉 ⇒* 〈STOP, m_end 〉 ->
        〈c, s 〉 ⇒* 〈STOP, s_end 〉 ->
            state_low_eq Γ m_end s_end.

---

ChangeLog

2026-06-03: Build with dune

Changed

• Migrated the build from the rocq makefile-generated Makefile to dune's Rocq build language (dune-project + dune with (rocq.theory (name NI)) and (include_subdirs qualified)). dune build now compiles everything out-of-tree into _build/, keeping the source directory free of .vo/.glob/... artifacts.
• Removed the old Makefile and _CoqProject (superseded by the dune files); .dir-locals.el now points Proof General at _build/default.

2026-06-03: Port to the Rocq Prover 9.2

Changed

• Updated the development to build with the Rocq Prover 9.2 (post Coq→Rocq renaming).
• Standard-library imports now use the From Stdlib Require ... form (the stdlib is a separate package since Rocq 9.0).
• Replaced the removed Omega library / omega tactic with Lia / lia.
• Replaced the removed Implicit Arguments command with Arguments, the removed no-argument instantiate and elimtype tactics, and the section-less Variable declaration in the bundled LibTactics.
• Updated the bundled SfLib to modern Nat.eqb lemmas and dropped the numbered solve by inversion N notations, whose literal numeric tokens are reserved as keywords by recent Rocq and would otherwise break parsing of numeric literals.
• Build driver now invokes rocq makefile / rocq doc instead of the renamed coq_makefile / coqdoc.

Removed all admits and axioms

• Trimmed the bundled SfLib (285 -> 81 lines) down to the items this development actually uses -- the Case/SCase and solve by inversion tactics and the relation, deterministic and ex_falso_quodlibet definitions -- deleting the unused Software-Foundations exercise material (the Admitted exercise lemmas, the toy ev/appears_in/next_nat/... inductives, the beq_id/partial_map/extend maps, and SfLib's own multi), as well as its admit : forall T, T definition.
• Replaced LibTactics's Axiom inj_pair2 with a proof (via Eqdep.EqdepTheory.inj_pair2) and removed the skip_axiom : False soundness hole, routing skip/admit/demo through the existential-variable implementation (which cannot close a proof unsoundly).
• The development now declares no Admitted, Axiom, or Parameter, and Print Assumptions TINI reports Closed under the global context: the top-level noninterference theorem is fully axiom-free.

Optional sem automation database

• Added a dedicated sem hint database (Create HintDb sem) holding the constructors of the semantic, typing and low-equivalence relations (eval, step, exp_has_level, cmd_has_type, event_step, val_low_eq, var_low_eq, state_low_eq). It is kept separate from core so that the existing crush/auto/eauto and LibTactics */~ automation is unchanged and every existing proof stays stable; new or refactored proofs can opt in with eauto with sem. (Putting these constructors in core was tried and rejected: it destabilised the auto-star-based proofs, and for the high-level bridge_step_num/multi relations it made automation synthesise wrong existential witnesses.)
• Used eauto with sem in two typing reconstructions where it pays off: the WHILE case of preservation_cfg and the IFB/WHILE typing build in NIBridge (the latter, a 6-line manual T_If/T_Seq/T_While/T_Skip construction, becomes by eauto with sem).

Modernized hint declarations

• Every Hint now specifies an explicit database and locality (#[export] ... : core, #[local] where appropriate), with Create HintDb for the Sec/SComp databases.
• Replaced the deprecated Focus/Unfocus vernaculars in LowEq.v with the N: { ... } goal selector.

2016-08-03: More simplifications.

Added

• High-level description of the proof architecture.

Changed

• Simplified the definition of Bridge relation.

2016-07-29: Adequacy and Standard TINI

Added

• Indexed multi-step relation
• Adequacy theorem for the indexed multi-step relation
• Preservation for bridge relation
• The proof of Standard TINI via adequacy and NI for bridge

2016-07-27: Simplifying proof structure and porting to 8.5

Added

• Added _CoqProject file and a better Makefile
• Including an updated version of LibTactics that compiles in 8.5

Changes

• Simplifying the way the bridge relation is formulated, reducing the overall size of the codebase.
• More automation.

2016-07-10: update to the next version of Cpdt tactics.

2015-04-04: initial version of the proof.