Skip to content

Bug Pattern Matching Tool using SMT Solver for Patch Transplantation

Notifications You must be signed in to change notification settings

prosyslab/patron

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

patron

Static Patch Transplantation Tool

1. Dependency

  • Opam
  • Sparrow (added to your $PATH)
  • Python3

2. How to Build

Run the following command to build Patron

$ ./build.sh

3. Prerequisites

3.1. Donor Programs: The Patch Donor

  • A pair of buggy and patched versions of the program
  • The donor project directory must have the following structure.
target_dir
    ├--bug
    │   ├ x.c
    │   └ sparrow-out 
    └--patch      ├ ...
        ├ y.c
        └ sparrow-out 
                ├ ...
  • Each .c file must be parsed into CIL format.
  • Run the following to parse your c program into cil_file (output saved at the same directory as the original c file).
$ ./bin/cil_parser path/to/your/c/file

3.2 Donee Program: The Patch Donee

  • A C Program with Sparrow Analysis Results
  • sparrow-out directory (output of Sparrow) must be within the same directory with the C Program.

Usage

0. Sparrow Analysis

First, make sure you analyze your donor programs and donee program.

To do so, run the following command

$ cd <Target Directory>
$ ./bin/sparrow [-io | -tio | -mio | -pio | -dz | -nd | -bo] <Target C Program>

Note that <Target Directry> is where your C file is located at.

The options indicate the following:

-io  : Analyze for Integer Overflow only
-tio : Analyze for Multiplication Integer Overflow only
-mio : Analyze for Subtraction Integer Overflow only
-pio : Analyze for Addition Integer Overflow only
-dz  : Analyze for Divide-by-zero only
-nd  : Analyze for Null Pointer Dereference only
-bo  : Analyze for Buffer Overflow only

1. Direct Transplantation from Donor to Donee

$ ./patron dtd <Donor Directory> <Donee Directory> <True Alarm #>

Here, Donor and Donee Directory are as described in the Prerequisites section.

True Alarm # refers to the alarm of the bug program under .../<Donor Directory>/bug/sparrow-out/taint/datalog.

Sparrow provides sparrow-out/taint/datalog/Alarm.map file that describes the line numbers and alarm numbers from the analysis results.

Find the true alarm number from the directories under .../<Donor Directory>/bug/sparrow-out/taint/datalog.

For example, You can run

$ ./test/sparrow-all   # analyze all the test programs 
$ ./patron dtd test/donors/example01/ test/example01_donee1 0

Then, patron-out directory is created. You can check the patch result at patron-out/result__0_diff.patch as

--- /root/patron-artifact-new/patron/patron-out/orig__0_0.c	2024-12-31 14:09:43.068967624 +0900
+++ /root/patron-artifact-new/patron/patron-out/patch__0_0.c	2024-12-31 14:09:43.068967624 +0900
@@ -1,7 +1,7 @@
 /* Generated by CIL v. 1.7.4 */
 /* print_CIL_Input is false */
 
 extern int ( /* missing proto */  getchar)() ;
 #line 1 "main.c"
 int main(void) 
@@ -32,6 +32,9 @@
 #line 11
     return (1);
   }
+  if ((int )x * (int )y > 127) {
+    return (1);
+  }
 #line 13
   c = (char )((int )x * (int )y);
 #line 15

Note that the alarm must correspond to the bug that is patched by the donor patched program

2. Database Construction and Application of the Database

Patron also provides features to construct a pattern database.

Run the following.

$ ./patron db <Donor Directory> <True Alarm #>

For example, Running

$ ./test/sparrow-all   # analyze all the test programs 
$ ./patron db test/donors/example01/ 0

will generate patron-DB directory.

If you continue running this command with other donor programs, the pattern gets accumulated into patron-DB

Then, you can run

$ ./patron patch <Donee Directory>

For example,

$ ./patron patch test/example01_donee1

Then you get the same results as the direct transplantation in the previous section.

Debugging

The patron-out directory provides several files including encoding details for Z3 solver and output of the solver

For example,

  • <Alarm #>_ans.smt2 and <Alarm #>_sol.map are the raw results of solver.
  • diff is the AST diff result.
  • log.txt is the log file.
  • buggy_numer_formula is the encoded logical formula for the solver.

About

Bug Pattern Matching Tool using SMT Solver for Patch Transplantation

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Contributors 3

  •  
  •  
  •  

Languages