janislley/lsverifier

LSVerifier - Large Systems Verifier

LSVerifier

LSVerifier is a command-line tool for formal verification of large ANSI-C projects in a single run.

It leverages the ESBMC model checker as its core verification engine.

Demo video.

Version

Version	Improviments
v0.3.0	Support specific class of property verification; Support for large software; Prioritized functions verification, Disable invalid pointer verification.
v0.2.0	Support for libraries dependencies; Recursive verification.

Requirements

Ctags is required to use LSVerifier.

Installation

Install LSVerifier

From repository

1. Clone the repository:

$ git clone https://github.com/janislley/lsverifier.git

2. Install using pip:

$ cd LSVerifier
$ pip3 install .

From Pypi

$ pip3 install lsverifier

Usage

1. Verify a project

$ cd <project-root>
$ lsverifier -r -f

For projects with third-party library dependencies, use -l option to specify header paths:

$ lsverifier -r -f -l dep.txt

See an example of dep.txt below:

  /usr/include/glib-2.0/
  /usr/lib/x86_64-linux-gnu/glib-2.0/include/extcap/
  extcap/
  plugins/epan/ethercat/
  plugins/epan/falco_bridge/
  plugins/epan/wimaxmacphy/
  epan/crypt/
  ...

2. Verify a single C file

$ lsverifier -f -fl file.c

3. Verify C files using a priorization algorithm

If you want to verify a project using a prioritization scheme, run:

$ cd <project-root>
$ lsverifier -r -fp

4. Verify an entire project by providing the folder path as an argument

To set the folder path parameter, you should use -d:

lsverifier -r -f -l dep.txt -d project-root/

5. Verify C files using a predefined class of properties

In the project that you want to verify, run:

$ lsverifier -r -f -p memory-leak-check,overflow-check,deadlock-check,data-races-check

See more properties on tool help.

6. LSVerifier help

For more details, check the help:

$ lsverifier -h

usage: lsverifier [-h] [-l LIBRARIES] [-p PROPERTIES] [-f] [-fp] [-fl FILE] [-v] [-r] [-d DIRECTORY] [-dp] [-e ESBMC_PARAMETER]

Input Options

optional arguments:
  -h, --help            show this help message and exit
  -l,--libraries LIBRARIES
                        Path to the file that describes the libraries' dependencies
  -p,--properties PROPERTIES
                        Properties to be verified (comma separated):
                        multi-property
                        nan-check
                        memory-leak-check
                        floatbv
                        overflow-check
                        unsigned-overflow-check
                        ub-shift-check
                        struct-fields-check
                        deadlock-check
                        data-races-check
                        lock-order-check
  -f, --functions       Enable Functions Verification
  -fp, --function-prioritized
                        Enable Prioritized Functions Verification
  -fl,--file FILE       File to be verified
  -v, --verbose         Enable Verbose Output
  -r, --recursive       Enable Recursive Verification
  -d,--directory DIRECTORY
                        Set the directory to be verified
  -dp, --disable-pointer-check
                        Disable invalid pointer property verification
  -e,--esbmc-parameter ESBMC_PARAMETER
                        Use ESBMC parameter

Verification report

The verification results will be saved in output folder, automatically created in the current verification path. Each verification run generates two files:

• lsverifier-DATE.log: Contains the verification output log.
• lsverifier-DATE.csv: Contains the verification results in CSV format.

lsverifier's Issues

Is not possilble to verify recursively

There is not a way to verify the code recursively neither choose the folder to be verified.

After enable stderr, PUTTY verification freezes

Problem

Running the script using below command to verify PUTTY application, the verification freezes.
The problem occurs on termina.c file and paste_from_clip_local.

Logs

esbmc-wr log

Not unwinding loop 33 iteration 1 file terminal.c line 708 function compressline
**** WARNING: no body for function BinarySource_get_byte
Not unwinding loop 34 iteration 1 file terminal.c line 721 function compressline
**** WARNING: no body for function BinarySource_get_byte
Not unwinding loop 5 iteration 1 file string.c line 308 function memcmp
**** WARNING: no body for function BinarySource_get_uint16
Not unwinding loop 5 iteration 1 file string.c line 308 function memcmp
**** WARNING: no body for function BinarySource_get_byte
Not unwinding loop 30 iteration 1 file terminal.c line 477 function makerle
**** WARNING: no body for function BinarySource_get_uint16
Not unwinding loop 31 iteration 1 file terminal.c line 426 function makerle
**** WARNING: no body for function BinarySource_get_uint32
Not unwinding loop 5 iteration 1 file string.c line 308 function memcmp
**** WARNING: no body for function BinarySource_get_byte
Not unwinding loop 5 iteration 1 file string.c line 308 function memcmp
**** WARNING: no body for function BinarySource_get_uint16
Not unwinding loop 30 iteration 1 file terminal.c line 477 function makerle
**** WARNING: no body for function BinarySource_get_uint16 
Not unwinding loop 31 iteration 1 file terminal.c line 426 function makerle
**** WARNING: no body for function BinarySource_get_uint16 1

esbmc log

Not unwinding loop 97 iteration 1 file terminal.c line 3118 function term_print_flush                          
**** WARNING: no body for function ldisc_send                                                                  
**** WARNING: no body for function safefree                                                                    
**** WARNING: no body for function queue_toplevel_callbackNot unwinding loop 59 iteration 1 file terminal.c line 1491 function term_seen_key_event
                                                                                                               
**** WARNING: no body for function strbuf_free                                                                 
**** WARNING: no body for function safefree                                                                    
**** WARNING: no body for function ldisc_send                                                                  
**** WARNING: no body for function queue_toplevel_callback                                                     
Symex completed in: 605.319s (164811 assignments)                                                              
No solver specified; defaulting to Boolector                                                                   
Slicing time: 3.255s (removed 64842 assignments)                                                               
Generated 70278 VCC(s), 54059 remaining after simplification (99969 assignments)                               
terminate called after throwing an instance of 'std::bad_cast'                                                 
  what():  std::bad_cast  

Execution doesn't finish while analyzing Putty 0.78

Steps to reproduce:

• Download putty 0.78 available at: https://github.com/janislley/lsverifier_final_results
• Run lsverifier with:

$ cd putty-0.78
$ lsverifier -v -r -f -fl terminal/terminal.c -l dep.tx

Is not possible to check only a file

There is not a way to verify all function of a single file.

TypeError: __init__() got an unexpected keyword argument 'text'

I've just wanted to run 'esbmc-wr' and got the following error.
TypeError: __init__() got an unexpected keyword argument 'text'
When i was going to verify one c file.