Keep track of internal contexts

[LeventErkok]

[Discovered in collaboration with Ian Blumenfeld. Thanks Ian!]

Since the symbolic monad is an instance of MonadIO; it's possible to embed IO actions as we run through: This is useful for debugging. However, it also allows for the prover to make a nested call, which can acquire variables from the surrounding context. Of course, this will never work, since the inner context doesn't know about the definitions of the surrounding context. We should definitely catch and report this as "unsupported": Currently, we just spit out some SMT-Lib, which may or may not be correct. Clearly this is dangerous, as it can create soundness issues. The solver can return a result on the translation, which will have nothing to do with the intended meaning of the query.

Here's a piece of code to demonstrate the issue:

import Data.SBV
import Control.Monad.Trans

f :: SWord32 -> SWord32 -> IO SBool
f x y = do
  res <- isSatisfiableWith cvc4{verbose=True} (Just 10) $ (x .== y)
  case res of
    Just x    -> return (if x then true else false)
    Nothing   -> return false

bug = proveWith cvc4{verbose=True} $ do
  x <- free "x"
  y <- free "y"
  liftIO $ f x y

[LeventErkok]

NB. In the above example, if "f" has only one argument (drop the "y"), we get a valid program as output since "s0" happens to be available in the outer context as well. This is really dangerous, and should be addressed with a mechanism not unlike runST's escape handling, if possible. (Otherwise, we might have to add some notion of a thread id and check creation/use is done in the same thread dynamically. Not ideal, but better than nothing.)

[LeventErkok]

Things have changed since 2015, but this bug is still there! Here's the new program to exhibit this very same behavior:

import Data.SBV
import Control.Monad.Trans

f :: SWord32 -> SWord32 -> IO SBool
f x y = do r <- isSatisfiableWith z3{verbose=True} (x .== y)
           return (literal r)

bug = proveWith z3{verbose=True} $ do
  x <- free "x"
  y <- free "y"
  liftIO $ f x y

[LeventErkok]

Now in 2019, Also possible to create this using queries:

import Data.SBV
import Data.SBV.Control

import Control.Monad.Trans

leak :: IO SBool
leak = runSMT $ do x <- sBool "x"
                   query $ pure x

terrible :: IO ThmResult
terrible = proveWith z3{verbose=True} $ do
        y <- sBool "y"
        x <- lift leak        -- reach in!
        return $ y .== x

This is a soundness bug, terrible is an SBV theorem, but it doesn't even make sense as a program.