Using CrossHair to convert simple functions into Z3 expressions to verify time sensitive applications

[asrv]

Hi Phillip,

I'm trying to formally verify simple functions that are time sensitive using CrossHair. The goal is to find path(s) of a given function that verifies a property p and the symbolic values of the returned variables. This is a quite similar to issue #142 .

Here's an example:

def f(t:int,a:bool) -> bool :
    if t>10:
        return a
    else:
        return not a

Property p is : there exists a t greater than 5 such that a is true.

Context:

I use this in SVSHI, an open-source smart-home hub that runs applications in Python that are formally verified to avoid conflicts between two applications.
These applications are short and run periodically.
Each application has its own properties and we use CrossHair to check if these properties are satisfied.
The next step to enhance the verification is to manage time sensitive properties.

We provide an API to give time to the developer, by using multiples variables for the seconds, minutes, hour etc.. to avoid using non-linear arithmetic.

Then we can create properties that are time-sensitive using these variables. Example : Every two days a (where a is a physical switch) is True for two minutes. Here we can suppose that t is a variable that represent a minute, where 0<=t<=59
However, when using CrossHair we couldn't have a "memory" a previous execution and this always lead to counterexamples.

A solution I found is to modify slightly the cover function to return the solver at the end of run_iteration and get the return values from the function to symbolic values.

Then I recreate a function in Z3 using all the output of crosshair and then use Z3's solver to verify the property.

Details of the modifications:

Getting the symbolic variables in path_cover here by getting the "var" attribute (thanks to @lmontand !)

Getting the paths constraints from the StateSpace object after detaching the path
It's is copied and put into a list with the return values.

Then I run the path_cover function to get everything from a specific function.

To get back to the example of the function, CrossHair will output these paths [[Not(10 < t_2), Not(a_3)], {'ret': True}]
[[10 < t_2], {'ret': a_3}]
[[Not(10 < t_2), a_3], {'ret': False}]
Then they are converted to Z3 expression and I can use this to verify any properties.

Something I haven't figured out yet is when you have a boolean variable with not as a return, it seems to realize (hence the two 'paths' when t<10). But it is still working as intended, which is the most important!

Let me know if you have any suggestions, improvements or seeing any limitations.
Also a big thank you for providing this tool, it's very helpful and it doing very well for the symbolic execution :)

Cheers,
Aymeri

[pschanely]

First, it's really exciting to see CrossHair in action here!

Comments follow, some of which I've broken into other discussions/bugs, in no particular order:

1. I've just filed an issue discussing the not operator realizing values: Add symbolic support for not #167
2. The various points you've hooked into CrossHair make sense; I'm glad that the code wasn't so obscure so as to make it impossible! Obviously these points aren't part of any officially supported API, so you'll have to maintain (or freeze) a CrossHair fork. Still, someday, something like Obtain symbolic values and path conditions without concretization after path_cover for post-testing analysis #142 might happen; significant challenges remain to do this in the general case, as perhaps only integers and booleans have Z3 modelings that are obvious.
3. I've also added a brief discussion about proving existentially quantified properties: Contracts with existential quantification #166. I am curious how similar that problem is to yours. I might imagine that finding two time periods for which a switch is on could be done with something like this crosshair-web example. Perhaps the real challenge lies in the fact that you need to find very many such inputs (120 for two minutes?).

[asrv]

Hi Phillip,

Thanks for your reply!

Indeed for point 2, we made a fork here. It was easy for us as we only have simple types (int, float and bool). I would imagine that with classes it seems like a much more complex task.

For point 3., we tried your list approach and as you pointed out we need many inputs. Generating an extensive list would lead to timeouts (on my computer, a list of more than 6 elements take more than 5 minutes for crosshair to terminate). We also model conditions that could hold for multiple hours and it gives a much larger list.
For the existential quantifier, finding a counterexample by negating the property works as you mentioned on #166. Sorry that I was not precise enough, we wanted to model a "there exists a condition c that holds for all input". In this case, we cannot negate the condition as we need to test the condition afterward. Hence the use of z3 expression to have full flexibility on the quantifiers.