From efea5c44759ecd99d124c0b557348ee57d364b5b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 May 2018 13:05:38 +0100 Subject: [PATCH 1/3] Fix flattening of access beyond type-specified bounds The test Pointer_byte_extract5 was previously only solved properly thanks to hacks in the simplifier. We should not have to rely on those. Also adjust the malloc size computation to not rely on absence of padding. --- regression/cbmc/Pointer_byte_extract5/main.c | 2 +- .../Pointer_byte_extract5/no-simplify.desc | 14 ++++++++ .../cbmc/Pointer_byte_extract5/test.desc | 5 +++ .../flattening/boolbv_byte_extract.cpp | 32 ++++++++++++++++--- src/solvers/flattening/boolbv_index.cpp | 24 +++++++++++++- 5 files changed, 71 insertions(+), 6 deletions(-) create mode 100644 regression/cbmc/Pointer_byte_extract5/no-simplify.desc diff --git a/regression/cbmc/Pointer_byte_extract5/main.c b/regression/cbmc/Pointer_byte_extract5/main.c index 7f95b4a5a03..dd4758852b2 100644 --- a/regression/cbmc/Pointer_byte_extract5/main.c +++ b/regression/cbmc/Pointer_byte_extract5/main.c @@ -22,7 +22,7 @@ typedef struct int main() { - Struct3 *p = malloc (sizeof (int) + 2 * sizeof(Union)); + Struct3 *p = malloc(sizeof(Struct3) + sizeof(Union)); p->Count = 3; int po=0; diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc new file mode 100644 index 00000000000..f93bcf98401 --- /dev/null +++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc @@ -0,0 +1,14 @@ +CORE +main.c +--bounds-check --32 --no-simplify +^EXIT=10$ +^SIGNAL=0$ +array\.List dynamic object upper bound in p->List\[2\]: FAILURE +\*\* 1 of 14 failed +-- +^warning: ignoring +-- +Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c. +C90 did not have flexible arrays, and using arrays of size 1 was common +practice: http://c-faq.com/struct/structhack.html. We need to treat those as if +it were a zero-sized array. diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc index fa59dbff9dc..ba7ae563823 100644 --- a/regression/cbmc/Pointer_byte_extract5/test.desc +++ b/regression/cbmc/Pointer_byte_extract5/test.desc @@ -7,3 +7,8 @@ array\.List dynamic object upper bound in p->List\[2\]: FAILURE \*\* 1 of 11 failed -- ^warning: ignoring +-- +Test is built from SV-COMP's memsafety/20051113-1.c_false-valid-memtrack.c. +C90 did not have flexible arrays, and using arrays of size 1 was common +practice: http://c-faq.com/struct/structhack.html. We need to treat those as if +it were a zero-sized array. diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 2515da21123..7979d086620 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -78,6 +79,30 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) if(width==0) return conversion_failed(expr); + // see if the byte number is constant and within bounds, else work from the + // root object + const mp_integer op_bytes = pointer_offset_size(expr.op().type(), ns); + auto index = numeric_cast(expr.offset()); + if( + (!index.has_value() || (*index < 0 || *index >= op_bytes)) && + (expr.op().id() == ID_member || expr.op().id() == ID_index || + expr.op().id() == ID_byte_extract_big_endian || + expr.op().id() == ID_byte_extract_little_endian)) + { + object_descriptor_exprt o; + o.build(expr.op(), ns); + CHECK_RETURN(o.offset().id() != ID_unknown); + if(o.offset().type() != expr.offset().type()) + o.offset().make_typecast(expr.offset().type()); + byte_extract_exprt be( + expr.id(), + o.root_object(), + plus_exprt(o.offset(), expr.offset()), + expr.type()); + + return convert_bv(be); + } + const exprt &op=expr.op(); const exprt &offset=expr.offset(); @@ -106,13 +131,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) // see if the byte number is constant unsigned byte_width=8; - mp_integer index; - if(!to_integer(offset, index)) + if(index.has_value()) { - if(index<0) + if(*index < 0) throw "byte_extract flatting with negative offset: "+expr.pretty(); - mp_integer offset=index*byte_width; + const mp_integer offset = *index * byte_width; std::size_t offset_i=integer2unsigned(offset); diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index ff63fedf14e..ba5b70e52b8 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -11,8 +11,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include +#include bvt boolbvt::convert_index(const index_exprt &expr) { @@ -333,6 +334,27 @@ bvt boolbvt::convert_index( for(std::size_t i=0; i Date: Mon, 7 May 2018 14:04:05 +0000 Subject: [PATCH 2/3] Handle negative byte_extract offsets These are just out-of-bounds accesses. --- src/solvers/flattening/boolbv_byte_extract.cpp | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 7979d086620..b489a9b1924 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -133,19 +133,14 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) if(index.has_value()) { - if(*index < 0) - throw "byte_extract flatting with negative offset: "+expr.pretty(); - const mp_integer offset = *index * byte_width; - std::size_t offset_i=integer2unsigned(offset); - for(std::size_t i=0; i=op_bv.size()) + if(offset + i < 0 || offset + i >= op_bv.size()) bv[i]=prop.new_variable(); else - bv[i]=op_bv[offset_i+i]; + bv[i] = op_bv[numeric_cast_v(offset) + i]; } else { From d3d888bb075ec916918186b56699d381d3ea7af5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 23 May 2018 18:49:34 +0100 Subject: [PATCH 3/3] Bounds check for flexible array members Example crafted by Martin, which now clarifies which bounds we check: 1) When the object is stack-allocated and does not use flexible array members, the bounds are as specified in the type. 2) When flexible array members are used (zero-sized array), the semantics laid out in the standard are used (the bound is the size of the full object). 3) When the allocation size does not match the type-specified size (necessarily a case of heap allocation), use the size of the allocation. --- regression/cbmc/bounds_check1/main.c | 115 ++++++++++++++++++++++++ regression/cbmc/bounds_check1/test.desc | 14 +++ src/analyses/goto_check.cpp | 21 +++++ 3 files changed, 150 insertions(+) create mode 100644 regression/cbmc/bounds_check1/main.c create mode 100644 regression/cbmc/bounds_check1/test.desc diff --git a/regression/cbmc/bounds_check1/main.c b/regression/cbmc/bounds_check1/main.c new file mode 100644 index 00000000000..7f6fb231209 --- /dev/null +++ b/regression/cbmc/bounds_check1/main.c @@ -0,0 +1,115 @@ +#include +#include + +typedef struct _eth_frame_header +{ + uint8_t dest[6]; + uint8_t src[6]; + uint16_t length; + uint8_t payload[0]; +} eth_frame_header; + +typedef struct _eth_frame_header_with_tag +{ + uint8_t dest[6]; + uint8_t src[6]; + uint32_t tag; + uint16_t length; + uint8_t payload[0]; +} eth_frame_header_with_tag; + +typedef struct _eth_frame_footer +{ + uint32_t crc; +} eth_frame_footer; + +#define FRAME_LENGTH \ + sizeof(eth_frame_header_with_tag) + 1500 + sizeof(eth_frame_footer) + +typedef union _eth_frame { + uint8_t raw[FRAME_LENGTH]; + eth_frame_header header; + eth_frame_header_with_tag header_with_tag; +} eth_frame; + +typedef struct _eth_frame_with_control +{ + eth_frame frame; + uint32_t control; // Routing, filtering, inspection, etc. +} eth_frame_with_control; + +void stack() +{ + eth_frame_with_control f; + unsigned i, i2, j, j2, k, k2, l, l2; + + // Safe if 0 <= i < FRAME_LENGTH, viable attack over FRAME_LENGTH + __CPROVER_assume(i < FRAME_LENGTH); + // within array bounds + f.frame.raw[i] = 42; + __CPROVER_assume(i2 < FRAME_LENGTH + 4); + // possibly out-of-bounds, even though still within the object + f.frame.raw[i2] = 42; + + // Safe if 0 <= j < 6, likely unsafe if over 6 + __CPROVER_assume(j < 6); + // within array bounds + f.frame.header.dest[j] = 42; + // possibly out-of-bounds + f.frame.header.dest[j2] = 42; + + // Safe if 0 <= k < 1500, could corrupt crc if k < 1508, viable attack over 1508 + __CPROVER_assume(k < FRAME_LENGTH - 14); + // within array bounds + f.frame.header.payload[k] = 42; + // possibly out-of-bounds + f.frame.header.payload[k2] = 42; + + // Safe if 0 <= l < 1504, wrong but probably harmless if l < 1508, viable attack over 1508 + __CPROVER_assume(l < FRAME_LENGTH - 14); + // within array bounds + ((eth_frame_footer *)(&(f.frame.header.payload[l])))->crc = 42; + // possibly out-of-bounds + ((eth_frame_footer *)(&(f.frame.header.payload[l2])))->crc = 42; +} + +void heap() +{ + eth_frame_with_control *f_heap = malloc(sizeof(eth_frame_with_control)); + unsigned i, i2, j, j2, k, k2, l, l2; + + // Safe if 0 <= i < FRAME_LENGTH, viable attack over FRAME_LENGTH + __CPROVER_assume(i < FRAME_LENGTH); + // within array bounds + f_heap->frame.raw[i] = 42; + __CPROVER_assume(i2 < FRAME_LENGTH + 4); + // possibly out-of-bounds, even though still within the object + f_heap->frame.raw[i2] = 42; + + // Safe if 0 <= j < 6, likely unsafe if over 6 + __CPROVER_assume(j < 6); + // within array bounds + f_heap->frame.header.dest[j] = 42; + // possibly out-of-bounds + f_heap->frame.header.dest[j2] = 42; + + // Safe if 0 <= k < 1500, could corrupt crc if k < 1508, viable attack over 1508 + __CPROVER_assume(k < FRAME_LENGTH - 14); + // within array bounds + f_heap->frame.header.payload[k] = 42; + // possibly out-of-bounds + f_heap->frame.header.payload[k2] = 42; + + // Safe if 0 <= l < 1504, wrong but probably harmless if l < 1508, viable attack over 1508 + __CPROVER_assume(l < FRAME_LENGTH - 14); + // within array bounds + ((eth_frame_footer *)(&(f_heap->frame.header.payload[l])))->crc = 42; + // possibly out-of-bounds + ((eth_frame_footer *)(&(f_heap->frame.header.payload[l2])))->crc = 42; +} + +int main() +{ + stack(); + heap(); +} diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc new file mode 100644 index 00000000000..efec610daee --- /dev/null +++ b/regression/cbmc/bounds_check1/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--bounds-check --pointer-check +^EXIT=10$ +^SIGNAL=0$ +\[\(signed long( long)? int\)i2\]: FAILURE +dest\[\(signed long( long)? int\)j2\]: FAILURE +payload\[\(signed long( long)? int\)[kl]2\]: FAILURE +\*\* 10 of 72 failed +-- +^warning: ignoring +\[\(signed long( long)? int\)i\]: FAILURE +dest\[\(signed long( long)? int\)j\]: FAILURE +payload\[\(signed long( long)? int\)[kl]\]: FAILURE diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index cbc93c75968..c6ecab855b7 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1213,6 +1213,27 @@ void goto_checkt::bounds_check( expr.array().id()==ID_member) { // a variable sized struct member + // + // Excerpt from the C standard on flexible array members: + // However, when a . (or ->) operator has a left operand that is (a pointer + // to) a structure with a flexible array member and the right operand names + // that member, it behaves as if that member were replaced with the longest + // array (with the same element type) that would not make the structure + // larger than the object being accessed; [...] + const exprt type_size = size_of_expr(ode.root_object().type(), ns); + + binary_relation_exprt inequality( + typecast_exprt::conditional_cast(ode.offset(), type_size.type()), + ID_lt, + type_size); + + add_guarded_claim( + implies_exprt(type_matches_size, inequality), + name + " upper bound", + "array bounds", + expr.find_source_location(), + expr, + guard); } else {