Verifying temporal properties. Need problems.

Discussion in 'Python' started by Bjorn Heimir Bjornsson, Apr 1, 2004.

  1. 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
     
    Bjorn Heimir Bjornsson, Apr 1, 2004
    #1
    1. Advertising

  2. Bjorn Heimir Bjornsson

    Yermat Guest

    Bjorn Heimir Bjornsson wrote:
    > 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
     
    Yermat, Apr 2, 2004
    #2
    1. Advertising

  3. 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
     
    Bjorn Heimir Bjornsson, Apr 3, 2004
    #3
  4. Bjorn Heimir Bjornsson

    Yermat Guest

    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
     
    Yermat, Apr 3, 2004
    #4
  5. Yermat <1.nerim.net> wrote in
    > 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
     
    Bjorn Heimir Bjornsson, Apr 6, 2004
    #5
  6. Bjorn Heimir Bjornsson

    Yermat Guest

    Bjorn Heimir Bjornsson wrote:
    > Yermat <1.nerim.net> wrote in
    >
    >>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


    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
     
    Yermat, Apr 6, 2004
    #6
    1. Advertising

Want to reply to this thread or ask your own question?

It takes just 2 minutes to sign up (and it's free!). Just click the sign up button to choose a username and then you can ask your own questions on the forum.
Similar Threads
  1. Hongzheng Wang

    Is there a temporal object created?

    Hongzheng Wang, Dec 8, 2003, in forum: C++
    Replies:
    5
    Views:
    390
    Rob Williscroft
    Dec 9, 2003
  2. jose luis fernandez diaz

    Template temporal value

    jose luis fernandez diaz, Aug 3, 2004, in forum: C++
    Replies:
    4
    Views:
    394
    Victor Bazarov
    Aug 4, 2004
  3. David
    Replies:
    0
    Views:
    889
    David
    Jun 18, 2008
  4. aitor

    Adding temporal role

    aitor, Sep 30, 2008, in forum: ASP .Net Security
    Replies:
    1
    Views:
    706
    Alexey Smirnov
    Oct 1, 2008
  5. Wes Gamble
    Replies:
    5
    Views:
    102
    Wes Gamble
    Aug 4, 2006
Loading...

Share This Page