ExtractFix

Beyond Tests: Program Vulnerability Repair via Crash Constraint Extraction

Overview

Automated program repair can be used to prevent exploitation of known security vulnerabilities by attackers. The large potential impact of security vulnerabilities means that the need to avoid incomplete or incorrect fixes is paramount. In this paper, we present a new mechanism for automatically generating provably correct repair of security vulnerabilities. Given a program vulnerability witnessed by some crashing input or exploit, our basic approach relies on extracting a constraint representation of the underlying cause of the crash. This crash constraint can then be propagated backward to guide program repair over the space of possible fix locations. Our method synthesizes patch that is guaranteed to avoid repeating the original crash, thereby repairing the program for all program inputs not limited to a specific test suite. As such, our approach helps address the test over-fitting problem (where a suggested repair fails to generalize beyond a given test suite). An implementation of our method (ExtractFix) built on top of the KLEE symbolic execution engine shows its efficacy in fixing a wide range of vulnerabilities/bugs on subjects taken from CVEs and Google's Open-source-systems OSS Fuzz framework.

Our tool can be downloaded from here.

Publications

  • Beyond Tests: Program Vulnerability Repair via Crash Constraint Extraction

    Xiang Gao, Bo Wang, Gregory J. Duck, Ruyi Ji, Yingfei Xiong, Abhik Roychoudhury

    Transactions on Software Engineering and Methodology (TOSEM), 2020

W3Schools

The patches generated by ExtractFix (24/30)

Noe that the line number in the raw data might be slightly different with the original program because our instrumentation insert code snippts into the original files.

Subject ID Patch Correctness Bug Report Developer Fix Raw data
Libtiff CVE-2016-5321 
     for (col = 0; col < imagewidth; col += tw){
-         for (s = 0; s < spp; s++)
+         for (s = 0; s < spp && s < 8; s++)
          {  /* Read each plane of a tile set into srcbuffs[s] */"
 Syntactic equivalent report d9783e4 data
Libtiff CVE-2014-8128 
    rows[0] = br + bpr*sy;
	err += step;
-   while (err >= limit)
+   while (err >= limit && nrows <256)
	    err -= limit;
	    sy++;
 Semantically equivalent report 3206e0c data
Libtiff CVE-2016-3186 
-  while ((count = getc(infile)) && count <= 255)        
+  while ((count = getc(infile)) && count >= 0 && count <= 255)
Syntactic equivalent report 1144235 data
Libtiff CVE-2016-5314 
 ---
Fail report 391e77f
Libtiff CVE-2016-9273 
 ---
Fail report d651abc
Libtiff bugzilla 2633 
//define global variable to record buffer size/base
-    malloc(size);
+    global_size_cp = size;
+    malloc(global_size_cp);

// patch based on predefined global buffer size/base 
-    for (; cc < tf_bytesperrow; cc += samplesperpixel) {
+    for (; cc < tf_bytesperrow && nc+3 < global_size_cp; 
+           cc += samplesperpixel) {
 Plausible report 5ed9fea data
Libtiff CVE-2016-10094 
//define global variable to record buffer size/base
-    malloc(size);
+    global_size_buffer = size;
+    malloc(global_size_buffer);

// patch based on predefined global buffer size/base 
     int retTIFFReadRawTile;
     /* Ignore EOI marker of JpegTables */
     _TIFFmemcpy(buffer, jpt, count - 2);
-    bufferoffset += count - 2;
+    bufferoffset = (-1+(global_size_buffer-count));
     /* Store last 2 bytes of the JpegTables */
 Plausible report c715336 data
Libtiff CVE-2017-7601 
+        if( td->td_bitspersample > 64 )
+        {
+            return (0);
+        }
 Plausible report 0a76a8 data
Libtiff CVE-2016-3623 
+    if (vertSubSampling == 0) return 1;
Semantically equivalent report bd024f0 data
Libtiff CVE-2017-7595 
+    if (sp->h_sampleing == 0) return 1;
Semantically equivalent report 47f2fb6 data
Libtiff bugzilla 2611 
-    if (cc%sp->bytes_per_line!=0)
+    if (sp->bytes_per_line == 0 || cc%sp->bytes_per_line!=0)
 Semantically equivalent report 43bc25 data
Binutils CVE-2018-10372 
//define global variable to record buffer size/base
-    signature = malloc(size);
+    global_size_signature = size;
+    signature = malloc(global_size_signature);
+    global_base_signature = signature;

// patch based on predefined global buffer size/base 
-    if (!do_display)
+    if (((!(!((0)==(do_display))))&&((8)<(global_size_signature))))
 Plausible report 6aea08 data
Binutils CVE-2017-15025 
     case DW_LNS_const_add_pc:
+    if (lh.line_range == 0)
+        return 0;
 Semantically equivalent report d8010d3 data
Libxml2 CVE-2016-1834 
-    if (len < 0))
+    if (len<0 || size < 0 || len>Max+size))
 Plausible report 8fbbf551 data
Libxml2 CVE-2016-1838 
//define global variable to record buffer size/base
-    malloc(size);
+    global_size_cur = size;
+    malloc(global_size_cur);

// patch based on predefined global buffer size/base 
-    if ((tlen > 0) && (xmlStrncmp(ctxt->input->cur, ctxt->name, tlen) == 0)) {
+    if (((((0)<(tlen))&&((xmlStrncmp(ctxtinputcur,ctxtname,tlen))==(0)))
+        &&((tlen)<(global_size_cur)))) {
        if (ctxt->input->cur[tlen] == '>') {
 Plausible report db07dd6 data
Libxml2 CVE-2016-1839 
 ---
Fail report a820dbe
Libxml2 CVE-2012-5134 
 if ((in_space) && (normalize)) {
-    while (buf[len - 1] == 0x20) len--;
+    while ((len > 0) && (buf[len - 1] == 0x20)) len--;    
 }
 buf[len] = 0;
Syntactic equivalent report 6a36fbe data
Libxml2 CVE-2017-5969 
-    	    if ((content->c2->type == XML_ELEMENT_CONTENT_OR) ||
-    	        ((content->c2->type == XML_ELEMENT_CONTENT_SEQ) &&
-    	        (content->c2->ocur != XML_ELEMENT_CONTENT_ONCE))
+    	    if ((content->c2 != NULL) &&
+                (content->c2->type == XML_ELEMENT_CONTENT_OR) ||
+    	        ((content->c2->type == XML_ELEMENT_CONTENT_SEQ) &&
+    	        (content->c2->ocur != XML_ELEMENT_CONTENT_ONCE))
 Syntactic equivalent report 94691dc8 data
Libjpeg CVE-2018-14498 
//define global variable to record buffer size/base
-    malloc(size);
+    global_size_cp = size;
+    malloc(global_size_cp);

// patch based on predefined global buffer size/base
+    if (t >= global_size_cp)
+         ERREXIT(cinfo);
     *outptr++ = colormap[0][t]; /* can omit GETJSAMPLE() safely */
 Plausible report cbe01e data
Libjpeg CVE-2018-19664 
---
Fail report 1ecd9a
Libjpeg CVE-2017-15232 
+    if (output_buf == NULL && num_rows) {
+        ERREXIT(0);
+    }
 Semantically equivalent report 1ecd9a5 data
Libjpeg CVE-2012-2806 
-  for (i = 0; i < cinfo->num_components; i++)
+  for (i = 0; i < 4; i++)
     cinfo->cur_comp_info[i] = NULL;
   for (i = 0; i < n; i++) {
     INPUT_BYTE(cinfo, cc, return FALSE);
     INPUT_BYTE(cinfo, c, return FALSE);
-    for (ci = 0, compptr = cinfo->comp_info; ci < cinfo->num_components;
+    for (ci = 0, compptr = cinfo->comp_info; ci < cinfo->num_components && ci < 4;
 Semantically equivalent report dd2b651 data
Coreutils Bugzilla 26545 
-    for (i = 3; i < size / 2; i *= 2)
+    for (i = 3; i <= size / 2; i *= 2)
         memcpy (r + i, r, i);
     if (i < size)
         memcpy (r + i, r, size - i);
 Syntactic equivalent report f4570a data
Coreutils GNUBug 25003 
     end = (k == n) ? file_size : k * (file_size / n);
-    if (initial_read != SIZE_MAX || start < initial_read)
+    if (start < initial_read){
         memmove (buf, buf + start, initial_read - start);
         initial_read -= start;
 Syntactic equivalent report 4954f79 data
Coreutils GNUBug 25023 
---
Fail report d91aee
Coreutils Bugzilla 19784 
---
Fail report 1d0f1b7
Jasper CVE-2016-8691 
+   if(cmpt->hstep)
+        return 0;
     cmpt->width = JPC_CEILDIV(dec->xend, cmpt->hstep) -
		  JPC_CEILDIV(dec->xstart, cmpt->hstep);
 Semantically equivalent report d8c2604 data
Jasper CVE-2016-9387 
+    if(dec->yend <= dec->tileyoff)
+        return -1;
     dec->numvtiles = JPC_CEILDIV(dec->yend - dec->tileyoff, dec->tileheight);
     dec->numtiles = dec->numhtiles * dec->numvtiles;
 Plausible report d91198a data
FFmpeg CVE-2017-9992 
//define global variable to record buffer size/base
-    frame = malloc(size);
+    global_size_frame = size;
+    frame = malloc(global_size_frame);
+    global_base_frame = frame;

// patch based on predefined global buffer size/base 
-    if (frame_end - frame < width + 3)
+    if (global_base_frame + global_size_frame - frame < width + 4)
         return AVERROR_INVALIDDATA;
         frame[0] = frame[1] =
Semantic equivalent report f52fbf4 data
FFmpeg Bugzilla-1404 
    h->sym_factor = h->dist[0] * h->scale_den[1];
+    if (h->sym_factor > 32768) {
+        return AVERROR_INVALIDDATA;
 Semantic equivalent report 279420b

People

Principal investigator

Developers