Symbolic Execution and undefined behaviour causes :sat and :prove to give wrong answers

[weaversa]

I can only guess that the symbolic execution engine is adding constraints that say "produce 0" for undefined behaviour such as divide by 0 and index out of bounds. Here are two strange test cases:

Cryptol> :sat (x:[4]) -> x/0 == 0
((x : [4]) -> x / 0 == 0) 0 = True
Cryptol> 0/0
division by 0

Cryptol> :sat (x:[4]) -> [1, 2, 3, 4]@x == 0
((x : [4]) -> [1, 2, 3, 4] @ x == 0) 6 = True
Cryptol> ((x : [4]) -> [1, 2, 3, 4] @ x == 0) 6
invalid sequence index: 6

The previous version of Cryptol also produces answers, but is very verbose about detecting 'safety violations'. I suggest adding something similar to the current version, as well as resurecting the old :safe command.

Cryptol> :sat \x -> (x:[4])/0 == 0
(\x -> (x:[4]) /0 == 0) 0x0
= "command line", line 1, col 16: divide by zero
** A safety violation was detected, use the ":safe" command to check for others.
*** ALERT: Run result does not match formal analysis.
*** This can be caused by strict safety semantics, showing up in
*** C and hardware translations.
*** Use :safe command to identify others

Cryptol> :sat \x -> [1 2 3 4]@(x:[4]) == 0
(\x -> [1 2 3 4]@(x:[4]) == 0) 0x4
= "command line", line 1, col 17: index of 4 is out of bounds
(valid range is 0 thru 3).
** A safety violation was detected, use the ":safe" command to check for others.
*** ALERT: Run result does not match formal analysis.
*** This can be caused by strict safety semantics, showing up in
*** C and hardware translations.
*** Use :safe command to identify others

[LeventErkok]

This is a consequence of the "completion" in SBV/SMT. All functions are completed; in particular x / 0 = 0. See: http://hackage.haskell.org/package/sbv-3.1/docs/Data-SBV.html#g:26

Cryptol-1 went to extreme lengths to identify safety conditions and explicitly check for them.. And it didn't always work due to backend related differences in strictness.

But there's nothing really hard about it, but it's quite a bit of work!

[weaversa]

As an easy first step, the counter example could be concretely run back
through the proof.

On Tue, Aug 12, 2014 at 9:06 PM, Levent Erkok [email protected]
wrote:

This is a consequence of the "completion" in SBV/SMT. All functions are
completed; in particular x / 0 = 0. See:
http://hackage.haskell.org/package/sbv-3.1/docs/Data-SBV.html#g:26

Cryptol-1 went to extreme lengths to identify safety conditions and
explicitly check for them.. And it didn't always work due to backend
related differences in strictness.

But there's nothing really hard about it, but it's quite a bit of work!

—
Reply to this email directly or view it on GitHub
#70 (comment).

[LeventErkok]

Yeah; but you could get a "false" theorem; for which you wouldn't have a counter-example to run with. Something like this:

Cryptol> :prove \x -> (x:[4])/0 == 0
Q.E.D.

[LeventErkok]

I gave this some thought and actually it wouldn't be too hard to implement an integrated :safe, since SBV already supports sBranch for simulation time calls to external solvers. So, it'd be something like (I'm making up the Cryptol AST):

simulate (DIV a b) = 
              sBranch
                    (b == 0) 
                    (error "Safety violation: Can't guarantee non-zero divisor in this context")
                    (SBV.div a b)

This won't give you a separate :safe command, but would reject symbolic simulation if there's a chance a "bad thing" could happen. I think this might even be preferable to the original system where :safe was completely separate from :prove and :sat.

If you guys implement this, we can also add a variant of sBranch which also gave you a model under which the violation does happen, I'm thinking of a function like:

sAssert :: SBool -> String -> a -> a

(for some more specific a probably) that you can freely sprinkle in your code. Then you can say:

sAssert (b /= 0) "Safety: division by 0" (SBV.div a b)

and SBV would print the model out automatically in case it found the condition is not-necessarily true.

Feel free to submit a patch!

[LeventErkok]

I added an implementation of sAssert to SBV: LeventErkok/sbv@cfddd9c

It currently simply spits out a model for the violation as it is detected during symbolic simulation. i.e., there's no way for Cryptol to get a hold on to the context and print the model in some more viable way. (Turns out doing the latter is really tricky!)

Might be worth playing around; if you guys are so inclined.

[dylanmc]

Ping!

[LeventErkok]

Pong?

Incidentally, I just released SBV3.2; which adds sAssertCont:

http://hackage.haskell.org/package/sbv-3.2/docs/Data-SBV.html#v:sAssertCont

Cryptol can use it to essentially implement :safe; and it also allows a custom continuation that actually receives a falsifying model for nice printing purposes.

[brianhuffman]

I'll probably wait until after we formalize some of Cryptol's denotational semantics (#45) before trying to tackle this. If our model of type Bit is the three-element domain {True, False, undefined}, then we might use a pair of SBools to model a Bit: one says whether the element is defined, and the other encodes True or False. I'll have to see whether sAssertCont maps nicely onto our denotational model, once it's nailed down; we might be able to make use of it instead.

[TomMD]

This appears to have fallen off the radar again. @brianhuffman current thoughts?

(I ask because my foolish bug on an otherwise quick tantrix cryptol solution was made more opaque by this issue)

[dylanmc]

Not off the radar, rather "on the roadmap." I predict 2016 will lay the foundations for fixing this, and also see the fix as well.

[brianhuffman]

My thoughts on this issue are unchanged since my comments from Nov 19 last year. We certainly don't want to accept "proofs" of programs that raise exceptions, but to implement this correctly we need to specify the strictness properties of all Cryptol language constructs. We'll also need to document the strictness semantics of SBV's assertion mechanism to see how we can use it.

[LeventErkok]

Just some thoughts.. It's really tricky to have the exception semantics "precisely" captured in symbolic execution: What if you have an if-then-else with one branch no exceptions and the other does? The issue is you don't know how to symbolically merge the two in general: Though you can go a long way before it becomes a real issue, the situation is just not clean.

In the mean time, I came to the rather humble conclusion that ":prove" should simply be a partial correctness proof: If it says yes, then the property is correct assuming there're no exceptions raised.

Then, a separate proof is run to find out if there are any such exceptions.

This keeps a clean separation of these two separate goals, and simplifies life.

This is what the Cryptol-1 implementation attempted in the SBV backend: There was a ":prove"/":sat" call; but also a separate ":safe" call.

I'd recommend Cryptol-2 adopting the same mechanism and keeping these two separate. Trying to do both at the same time ends up being a never ending fight with all sorts of weird behavior. Of course, if you want you can hook-up ":prove" to do both, in two different passes. The point is that you keep the two goals separately and attack them separately as well. There's a lot of code in Cryptol-1's SBV backend that keeps track of these "proof conditions" etc.; but it was never fully polished..

[dylanmc]

Brian will check out SBV's new features here, to determine whether it's "low hanging fruit" or not.

[robdockins]

Duplicate of #284