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/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 { diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 2515da21123..b489a9b1924 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,22 +131,16 @@ 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) - throw "byte_extract flatting with negative offset: "+expr.pretty(); - - mp_integer offset=index*byte_width; - - std::size_t offset_i=integer2unsigned(offset); + const mp_integer offset = *index * byte_width; 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 { 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