From 39a9350f6e3591b4062e3ea90f1ca1d1ca0ee626 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Mon, 7 Dec 2020 06:27:14 +0100 Subject: [PATCH] Bug hunting: Better analysis of BailoutValue --- lib/exprengine.cpp | 61 ++++++++++++++++++++--------------- test/testbughuntingchecks.cpp | 16 +++++++++ 2 files changed, 51 insertions(+), 26 deletions(-) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index b5f18fbee..9569ecc9e 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -1029,10 +1029,16 @@ std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const #ifdef USE_Z3 -struct ExprData { +class ExprData { +public: typedef std::map ValueExpr; typedef std::vector AssertionList; + class BailoutValueException: public ExprEngineException { + public: + BailoutValueException() : ExprEngineException(nullptr, "Incomplete analysis") {} + }; + z3::context context; ValueExpr valueExpr; AssertionList assertionList; @@ -1042,6 +1048,15 @@ struct ExprData { solver.add(assertExpr); } + void addConstraints(z3::solver &solver, const Data* data) { + for (auto constraint : data->constraints) { + try { + solver.add(getConstraintExpr(constraint)); + } catch (const BailoutValueException &) { + } + } + } + z3::expr addInt(const std::string &name, int128_t minValue, int128_t maxValue) { z3::expr e = context.int_const(name.c_str()); valueExpr.emplace(name, e); @@ -1108,6 +1123,8 @@ struct ExprData { z3::expr getExpr(ExprEngine::ValuePtr v) { if (!v) throw ExprEngineException(nullptr, "Can not solve expressions, operand value is null"); + if (v->type == ExprEngine::ValueType::BailoutValue) + throw BailoutValueException(); if (auto intRange = std::dynamic_pointer_cast(v)) { if (intRange->name[0] != '$') #if Z3_VERSION_INT >= GET_VERSION_INT(4,7,1) @@ -1162,7 +1179,6 @@ struct ExprData { } private: - z3::expr bool_expr(z3::expr e) { if (e.is_bool()) return e; @@ -1191,8 +1207,7 @@ bool ExprEngine::IntRange::isEqual(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addInt(name, minValue, maxValue); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, data); exprData.addAssertions(solver); solver.add(e == value); return solver.check() == z3::sat; @@ -1220,8 +1235,7 @@ bool ExprEngine::IntRange::isGreaterThan(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addInt(name, minValue, maxValue); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, data); exprData.addAssertions(solver); solver.add(e > value); return solver.check() == z3::sat; @@ -1249,8 +1263,7 @@ bool ExprEngine::IntRange::isLessThan(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addInt(name, minValue, maxValue); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, data); exprData.addAssertions(solver); solver.add(e < value); return solver.check() == z3::sat; @@ -1279,8 +1292,7 @@ bool ExprEngine::FloatRange::isEqual(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addFloat(name); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, data); exprData.addAssertions(solver); solver.add(e >= value && e <= value); return solver.check() != z3::unsat; @@ -1310,8 +1322,7 @@ bool ExprEngine::FloatRange::isGreaterThan(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addFloat(name); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, data); exprData.addAssertions(solver); solver.add(e > value); return solver.check() == z3::sat; @@ -1341,8 +1352,7 @@ bool ExprEngine::FloatRange::isLessThan(DataBase *dataBase, int value) const z3::solver solver(exprData.context); try { z3::expr e = exprData.addFloat(name); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, data); exprData.addAssertions(solver); solver.add(e < value); return solver.check() == z3::sat; @@ -1363,8 +1373,7 @@ bool ExprEngine::BinOpResult::isEqual(ExprEngine::DataBase *dataBase, int value) ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, dynamic_cast(dataBase)); exprData.addAssertions(solver); solver.add(e == value); return solver.check() == z3::sat; @@ -1382,8 +1391,7 @@ bool ExprEngine::BinOpResult::isGreaterThan(ExprEngine::DataBase *dataBase, int ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, dynamic_cast(dataBase)); exprData.addAssertions(solver); solver.add(e > value); return solver.check() == z3::sat; @@ -1405,8 +1413,7 @@ bool ExprEngine::BinOpResult::isLessThan(ExprEngine::DataBase *dataBase, int val ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, dynamic_cast(dataBase)); exprData.addAssertions(solver); solver.add(e < value); return solver.check() == z3::sat; @@ -1428,8 +1435,7 @@ bool ExprEngine::BinOpResult::isTrue(ExprEngine::DataBase *dataBase) const ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, dynamic_cast(dataBase)); exprData.addAssertions(solver); return solver.check() == z3::sat; } catch (const z3::exception &exception) { @@ -1449,8 +1455,7 @@ std::string ExprEngine::BinOpResult::getExpr(ExprEngine::DataBase *dataBase) con ExprData exprData; z3::solver solver(exprData.context); z3::expr e = exprData.getExpr(this); - for (auto constraint : dynamic_cast(dataBase)->constraints) - solver.add(exprData.getConstraintExpr(constraint)); + exprData.addConstraints(solver, dynamic_cast(dataBase)); exprData.addAssertions(solver); solver.add(e); std::ostringstream os; @@ -1767,7 +1772,11 @@ static void checkContract(Data &data, const Token *tok, const Function *function z3::solver solver(exprData.context); try { // Invert contract, we want to know if the contract might not be met - solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true))); + try { + solver.add(z3::ite(exprData.getConstraintExpr(data.executeContract(function, executeExpression1)), exprData.context.bool_val(false), exprData.context.bool_val(true))); + } catch (const ExprData::BailoutValueException &) { + throw ExprEngineException(tok, "Internal error: Bailout value used"); + } bool bailoutValue = false; for (nonneg int i = 0; i < argValues.size(); ++i) { @@ -1814,7 +1823,7 @@ static void checkContract(Data &data, const Token *tok, const Function *function } } catch (const z3::exception &exception) { std::cerr << "z3: " << exception << std::endl; - } catch (const ExprEngineException &e) { + } catch (const ExprEngineException &) { const char id[] = "internalErrorInExprEngine"; const auto contractIt = data.settings->functionContracts.find(function->fullName()); const std::string functionName = contractIt->first; diff --git a/test/testbughuntingchecks.cpp b/test/testbughuntingchecks.cpp index 5d7204fe8..a5ba043ea 100644 --- a/test/testbughuntingchecks.cpp +++ b/test/testbughuntingchecks.cpp @@ -39,6 +39,7 @@ private: TEST_CASE(arrayIndexOutOfBounds1); TEST_CASE(arrayIndexOutOfBounds2); TEST_CASE(arrayIndexOutOfBounds3); + TEST_CASE(arrayIndexOutOfBounds4); TEST_CASE(bufferOverflowMemCmp1); TEST_CASE(bufferOverflowMemCmp2); TEST_CASE(bufferOverflowStrcpy1); @@ -119,6 +120,21 @@ private: errout.str()); } + void arrayIndexOutOfBounds4() { // ensure there are warnings for bailout value + check("void foo(short i) {\n" + " int buf[8];\n" + "\n" + " data *d = x;\n" + " switch (d->layout) { case 0: break; }\n" + "\n" + " if (buf[i] > 0) {}\n" + "}"); + ASSERT_EQUALS("[test.cpp:7]: (error) Array index out of bounds, cannot determine that i is less than 8\n" + "[test.cpp:7]: (error) Array index out of bounds, cannot determine that i is not negative\n" + "[test.cpp:7]: (error) Cannot determine that 'buf[i]' is initialized\n", + errout.str()); + } + void bufferOverflowMemCmp1() { // CVE-2020-24265 check("void foo(const char *pktdata, int datalen) {\n"