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_hotmai l.com (more or less).

Thanks a lot :)
Bjorn

[Yermat]

Re: Verifying temporal properties. Need problems.

Bjorn Heimir Bjornsson wrote:[color=blue]
> 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_hotmai l.com (more or less).
>
> Thanks a lot :)
> Bjorn[/color]

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]

Re: Verifying temporal properties. Need problems.

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]

Re: Verifying temporal properties. Need problems.

Bjorn Heimir Bjornsson a écrit :
[color=blue]
> 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[/color]

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]

Re: Verifying temporal properties. Need problems.

Yermat <loic@yermat.ne t1.nerim.net> wrote in[color=blue]
> Instead of searching the workflow yourself you might look at PyPY.
> There is a class (see translator.py) that construct such a flow.[/color]

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.
[color=blue]
> On monday, I will show you a kind of workflow I'm creating in case
> mine is more complete than yours...[/color]

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

Bjorn

[Yermat]

Re: Verifying temporal properties. Need problems.

Bjorn Heimir Bjornsson wrote:[color=blue]
> Yermat <loic@yermat.ne t1.nerim.net> wrote in
>[color=green]
>>Instead of searching the workflow yourself you might look at PyPY.
>>There is a class (see translator.py) that construct such a flow.[/color]
>
>
> 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.
>
>[color=green]
>>On monday, I will show you a kind of workflow I'm creating in case
>>mine is more complete than yours...[/color]
>
>
> It would be really interesting to see what can be done with pypy's
> controlflow.
>
> Bjorn[/color]

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