Verifying temporal properties. Need problems.

[Bjorn Heimir Bjornsson]

Hello all

As part of a thesis, I am model checking Python programs (a limited
subset anyway).

I have a very rough prototype that can deal with temporal properties
(LTL), that is statically prove properties of the kind: "if A happens,
then B should follow" or "if A happens, then B must not follow unless
C happens first". A,B,C here being function calls (system or other
library). The idea is that this might complement testing or manual
auditing during development.

So the solution now requires a problem.
Basically I'm trying to find interesting areas where a programmer is
supposed to call specific functions in a particular order, but where
coding errors might prevent this.
I would be most happy with distinctively Python-related problems, like
some tricky-to-use system calls or something from Zope or
security-related issues, etc.

So if any of you have ideas (specific function calls) where this kind
of tool would be useful, I would welcome feedback.
If replying privately, use bjornhb2_hotmail.com (more or less).

Thanks a lot
Bjorn

 

[Yermat]

Hello all

As part of a thesis, I am model checking Python programs (a limited
subset anyway).

I have a very rough prototype that can deal with temporal properties
(LTL), that is statically prove properties of the kind: "if A happens,
then B should follow" or "if A happens, then B must not follow unless
C happens first". A,B,C here being function calls (system or other
library). The idea is that this might complement testing or manual
auditing during development.

So the solution now requires a problem.
Basically I'm trying to find interesting areas where a programmer is
supposed to call specific functions in a particular order, but where
coding errors might prevent this.
I would be most happy with distinctively Python-related problems, like
some tricky-to-use system calls or something from Zope or
security-related issues, etc.

So if any of you have ideas (specific function calls) where this kind
of tool would be useful, I would welcome feedback.
If replying privately, use bjornhb2_hotmail.com (more or less).

Thanks a lot
Bjorn

Hi,

I do not have any python program to check but I'm interested in
publications you might already have writen or pointers to python related
problem.
I'm working as engineer in a research team in formal methods area
(http://www.loria.fr/equipes/model/).

Did you look at similar project with Java (like
http://bandera.projects.cis.ksu.edu/) ? I think you will find similar
problem, no ?

Did your prototype recognize use of the thread standard library (lock,
etc) ?

If you look at mailman (http://www.list.org/), you can check security
property like "a non-members cannot send messages to the list", etc.

Do you look at rather small or big project ?

Sorry if I ask more question than I answer... ;-)
The last one : When will you finish your Phd ?

Loïc

 

[Bjorn Heimir Bjornsson]

Hello Loic
I'm working with control flow only, generating pushdown systems from the
AST that are then checked with the model checker Moped (using LTL
properties).
A similar approach was taken for JavaCard
(http://www.sics.se/fdt/vericode/jcave.html).
I chose Python for fun, but at the moment support just a limited subset.
I'm unsure how far I will/can go. E.g. some dynamic stuff can't be analysed
statically. I also just ignore all data flow, which simplifies everything but
means I will not recognise all control flow correctly.
I checked some small non-python-specific problems, but experience of others
suggest that the aproach scales quite well.
This is an MSc thesis, I haven't published anything else.
Bjorn

 

[Yermat]

Bjorn Heimir Bjornsson a écrit :

Hello Loic
I'm working with control flow only, generating pushdown systems from the
AST that are then checked with the model checker Moped (using LTL
properties).
A similar approach was taken for JavaCard
(http://www.sics.se/fdt/vericode/jcave.html).
I chose Python for fun, but at the moment support just a limited subset.
I'm unsure how far I will/can go. E.g. some dynamic stuff can't be analysed
statically. I also just ignore all data flow, which simplifies everything but
means I will not recognise all control flow correctly.
I checked some small non-python-specific problems, but experience of others
suggest that the aproach scales quite well.
This is an MSc thesis, I haven't published anything else.
Bjorn

Hi,
Ok I see.
Instead of searching the workflow yourself you might look at PyPY. There
is a class (see translator.py) that construct such a flow. I have also
construct a simple data flow to check if a variable used was previously
defined.

On monday, I will show you a kind of workflow I'm creating in case mine
is more complete than yours...

Anyway, you're right that with dinamic stuff, analysis is difficult. But
with research like StarKiller (Type Inference) it should become more and
more easier...

I will wait for your publication ;-)

Loïc

 

[Bjorn Heimir Bjornsson]

Instead of searching the workflow yourself you might look at PyPY.
There is a class (see translator.py) that construct such a flow.

Thanks Loic for pointing out pypy's controlflow. I will check if I can use
it. I had searched for something like this for Python but never found
anything.

On monday, I will show you a kind of workflow I'm creating in case
mine is more complete than yours...

It would be really interesting to see what can be done with pypy's
controlflow.

Bjorn

 

[Yermat]

Thanks Loic for pointing out pypy's controlflow. I will check if I can use
it. I had searched for something like this for Python but never found
anything.




It would be really interesting to see what can be done with pypy's
controlflow.

Bjorn

Hi,
At http://www.fejoz.net/Loic/Divers, you will find a little example of
the output of PyPy and output of my own program.
There is also my own program which only use Python AST where as PyPY is
more concrete.

Good luck !
Loïc