Processing math: 100%

Hyperproperties

UCLID5 supports the verification of hyperproperties at both the module level and procedural level.

Verifying Module Hyperproperties

One of the major benefits of using UCLID5 is the native support for creating instances. This allows the user to instantiate multiple instances that produce the traces in a hyperproperty. In this section, we present an intuitive way to verify hyperproperties. In the following sections, we present additional sugar-syntax for proving hyperinvariants of modules.

As an example, consider a transition system A: A=(V,I,δ)=({(a,x)|aN,xN},{(a,0)|aN},{((a,x),(a,x+a))|a,a,xN})

with system input a, state variable x, the set of initial states I and the transition relation δ.

A hyperproperty one may wish to prove is that the system is deterministic given that the inputs are the same, which can be specified as: iN.(πi1.a=πi2.a)(πi1.x=πi2.x)

where π1,π2 are traces of the system A and πi1,πi2 are the i-th states of the trace π1,π2 respectively. We also write πi1.a to mean the value of the variable a at state πi1 and similarly for other other variable and traces.

To prove such a property, one would first define the transition system A like this

// Filename: a.ucl module A { input a: integer; var x: integer; init { x = 0; } next { x' = x + a; } }

and then create a main module which consists of the proof of the specification. The proof would consist of instantiating two traces of A, π1 and π2, and specifying the invariant iN.πi1.x=πi2.x. Note that the antecedent of the implication above is implicitly assumed when a is used as an input to both instances (and hence are always equal between the two traces).

// Filename: a_determinism.ucl module main { var a: integer; // Two instances of A instance pi1: A(a: (a)); instance pi2: A(a: (a)); // Hyperproperty invariant determinism: pi1.x == pi2.x; // Step both instances by executing them synchronously and havoc the input a next { havoc a; next(pi1); next(pi2); } // Use inductive model checking to prove the hyperproperty over infinite traces control { v = induction; check; print_results; } }

Simply run uclid a.ucl a_determinism.ucl to obtain the results.

% uclid a.ucl a_determinism.ucl Successfully instantiated 2 module(s). 2 assertions passed. 0 assertions failed. 0 assertions indeterminate. PASSED -> v: induction_base [Step #0] property determinism @ a_determinism.ucl, line 9 PASSED -> v: induction_step [Step #1] property determinism @ a_determinism.ucl, line 9 Finished execution for module: main.

Hyperinvariants

Alternatively, one may specify the hyperproperty of the module within the module itself as such:

// Filename: a_hyperinvariant.ucl module A { input a: integer; var x: integer; init { x = 0; } next { x' = x + a; } hyperinvariant[2] determinism: (a.1 == a.2) ==> (x.1 == x.2); control { v = bmc(10); check; print_results; } }

NOTE: UCLID5 only supports hyperinvariant checking for bounded model checking. To verify the module above, run uclid -m A a_hyperinvariant.ucl (this indicates to the solver to run the control block in module A, which defaults to main if not specified).

HyperAxioms

In addition to the hyperinvariant syntax, one can specify a hyperaxiom, which are assumptions over multiple traces at each step. Continuing with our running example, one may rewrite the antecedent of the specification as an axiom:

// Filename: a_hyperaxiom.ucl module A { input a: integer; var x: integer; init { x = 0; } next { x' = x + a; } hyperaxiom[2] same_inputs: (a.1 == a.2); hyperinvariant[2] determinism: (x.1 == x.2); control { v = bmc(10); check; print_results; } }

NOTE: Hyperaxioms are only supported for bounded model checking.

Verifying Procedural Hyperproperties / Modular Product Verification

Up to this point, procedural properties have been specified using modifies, requires and ensures using the module variables and procedure arguments. UCLID5 also supports the verification of hyperproperties of procedural code.

module main { procedure isGreaterThanOrEqual(p: integer, q:integer) returns (res: boolean) ensures ((res == true) ==> ( p >= q)); ensures ((res == false) ==> ( p < q)); ensures ((p.1 == p.2 && q.1 == q.2) ==> (res.1 == res.2)); //determinism { res = true; if( p < q) { res = false; } } control { v = verify(isGreaterThanOrEqual); check; print_results; } }

The example above proves that the isGreaterThanOrEqual to indicator function is deterministic based on the inputs specified by line 5:

ensures ((p.1 == p.2 && q.1 == q.2) ==> (res.1 == res.2)); //determinism

Similar to the hyperinvariant syntax, the variable of the i-th trace is referred to using the .i operator, where i is the trace number.

NOTE: As of current, procedural hyperproperties only support the verification of pure functions that do not modify module state.