Different verification results produced when there is only a variable name difference

[zpzigi754]

I have the same targets to verify where there is only the difference in a variable name (owner_map in the below). While they contain the exact same code logic and there is no place where the modified variable is used, the verification results are different for some reasons. I think that this is the bug in uclid, but I am not sure what is the root cause of this bug.

$ git diff expected unexpected 
diff --git a/TrustedAbstractPlatform/standard/modules/see-cpu.ucl b/TrustedAbstractPlatform/standard/modules/see-cpu.ucl
index a26af0e..8d737f6 100644
--- a/TrustedAbstractPlatform/standard/modules/see-cpu.ucl
+++ b/TrustedAbstractPlatform/standard/modules/see-cpu.ucl
@@ -9,7 +9,7 @@ var enclave_id   : tap_enclave_id_t;
 var regs         : regs_t;
 var pc           : linear_addr_t;
 var addr_valid   : linear_addr_valid_t;
-var owner_map    : linear_owner_map_t;
+var owner_map_test    : linear_owner_map_t; // XXX: this is the only line modified from the `expected` branch

Different results

[expected results]
smt/ctap-assertion-_____modules_tap-mod_ucl__line_1708-verif_measurement_proof_2:_verify_measurement_proof_part2-0004.smt unknown ----------
smt/ctap-assertion-_____modules_tap-mod_ucl__line_1708-verif_measurement_proof_2:_verify_measurement_proof_part2-0056.smt unknown ----------

[unexpected results]
smt/ctap-assertion-_____modules_tap-mod_ucl__line_1708-verif_measurement_proof_2:_verify_measurement_proof_part2-0004.smt verified.
smt/ctap-assertion-_____modules_tap-mod_ucl__line_1708-verif_measurement_proof_2:_verify_measurement_proof_part2-0011.smt verified.

As there is an explicit false assertion inserted, the expected results are correct.

$ sed -n 1707,1708p trusted-abstract-platform/TrustedAbstractPlatform/standard/modules/tap-mod.ucl
        call simple_test();
        assert false;

However, in the unexpected results, this false assertion is bypassed for some reasons.

Before the false assertion, the child module (see)'s one variable is simply modified.

$ sed -n 566,571p trusted-abstract-platform/TrustedAbstractPlatform/standard/modules/tap-mod.ucl 
procedure [noinline] simple_test()
    ensures (see.enclave_id != old(see.enclave_id));
    modifies see;
{
    call see.havoc_enclave_id();
}

$ sed -n 15,23p trusted-abstract-platform/TrustedAbstractPlatform/standard/modules/see-cpu.ucl 
procedure [noinline] havoc_enclave_id()
  ensures (enclave_id != old(enclave_id));
  modifies enclave_id;
{
  var new_enclave_id : tap_enclave_id_t;
  havoc new_enclave_id;
  assume (new_enclave_id != enclave_id);
  enclave_id = new_enclave_id;
}

How to reproduce?

In the following two branches, expected-branch and unexpected-branch,

cd trusted-abstract-platform/TrustedAbstractPlatform/standard/proofs
$ make measurement-proof-printed
$ run_all_smt.sh

[polgreen]

Thanks for the report.

Can you explain to me why you think the expected result of "unknown" is correct? The ground truth is that the file is either SAT (fails verification) or UNSAT (passes verification), unknown is simply what the SMT solver reports when it can't figure out the actual answer.

I don't know why the SMT solver can find a solution in the second case but not in the first, I'll look into it, but note that if an "assert false" is unreachable, it will pass verification.

[zpzigi754]

Thank you for the answer. Whenever assert false; statement could be reached in a path, uclid seems to generate an unknown (==UNDEF) result.

In the above examples, the point before call simple_test(); (line 1706) is always reachable. Thus, if simple_test() procedure is not malfunctioning, the point after call simple_test(); should be also reachable (line 1708), which is assert false;. I thought that [expected results] are generated, because assert false is reached as expected.

In contrast, while the same procedure is called and all the assumptions are the same, the assert false in line 1708 is not reached in the [unexpected results].

I am not sure why assert false is unreachable in the second case (unexpected results).

[polgreen]

I think you have misunderstood the UNDEF/unknown results. All that means is that the SMT problem is too hard for the SMT solver to solve so we don't know whether your assert false is reachable or not. The correct result cannot ever be "undef" because the correct result is never "we don't know".

To summarise, for an assert false, if UCLID reports:

• verification failed (sat) - the assertion is definitely reachable
• verification passed (unsat) - the assertion is definitely unreachable
• undef (unknown) - the problem is too hard for the SMT solver. We don't know the answer.

We do not know if the line before simple_test is reachable either, because an assert false in that position is reported as UNDEF.

Take a look at the SMT files. The reason the files generated by your first branch are unknown is because there are a lot of difficult quantifiers. This is a much simplified version of part of one of your queries and an SMT solver reports unknown:

(set-logic ALL)
(declare-fun f (Int) Int)
(assert (forall ((v1 Int) (v2 Int))
  (or (not (= (f v1)(f v2)))
         (= v1 v2))
))
(check-sat)

The reason the second file can be verified, is the final two assertions are trivial to solve:

(assert (not (and (= havoc_172_proof_op tap_proof_op_enter) (not havoc_95_done))))
(assert (and (= havoc_172_proof_op tap_proof_op_enter) (not havoc_95_done)))

Without going into your proofs in detail, I'm not sure where these conflicting assertions have come from. I am happy to take a look if you can provide a more minimal input

[zpzigi754]

Thank you for the detailed answer. I seem to have misunderstood the UNDEF/unknown results.

I've made another example, but removed it because there was a logic error in that example.