Pharos batch commit July 5, 2022

This version of Pharos requires a more recent version of SWI Prolog:
v8.5.12.

* Adjustments for new versions of ROSE
* Fix problem with definers in LEA instructions
* Introduce a new fact, thisPtrDefinition, that will assist with future facts describing how to access virtual bases.
* New reasonObjectInObject_F rule
* Fix VFTableBelongsToClass rule
* Export information about inlined vftable writes
* Overhaul of the GTE_D rule
* Refine some rules to require negative offsets
* Add ability to lift symbolic expressions to Prolog

Fix #179
Fix #224
Fix #209
Fix #212
Fix #204

Author: sei-mwd

.dir-locals.el

@@ -1,6 +1,6 @@
 (
- (nil . ((indent-tabs-mode . nil)
-         (fill-column . 95)))
+ (nil . ((indent-tabs-mode . nil)))
+ (prog-mode . ((fill-column . 95)))
  (c-mode . ((c-basic-offset . 2)
             (c-block-comment-prefix . "")
             (comment-start . "// ")

.gitignore

@@ -50,3 +50,4 @@ local.cmake
 **/.tramp_history
 **/.tramp_ignore
 **/.gdb_history
+**/*/*.pdb

CMakeLists.txt

@@ -64,7 +64,8 @@ endif()
 
 # Rose
 
-# Anyone modifying this version should also manually modify libpharos/version.hpp.in.  They should set the PHAORS_ROSE_MINI
+# Anyone modifying this version should also manually modify libpharos/version.hpp.in.  They
+# should set the PHAROS_ROSE_MINIMUM_VERSION variable to match.
 set(PHAROS_ROSE_MINIMUM_VERSION 0.11.39.6)
 
 find_package(Rose ${PHAROS_ROSE_MINIMUM_VERSION} REQUIRED)

INSTALL.md

@@ -196,7 +196,7 @@ The latest release version of Z3 (4.8.7) has passed our testing.
 
 We build Z3 using commands like these:
 ```
-$ git clone -b Z3-4.8.7 https://github.com/Z3Prover/z3.git
+$ git clone -b z3-4.8.7 https://github.com/Z3Prover/z3.git
 $ cd z3
 $ mkdir build
 $ cd build
@@ -272,11 +272,11 @@ SWI Prolog version 8.3.19 or later fixes a bug in Prolog that can be
 triggered by ooanalyzer in some rare cases.  See
 https://github.com/cmu-sei/pharos/issues/156 for more details.
 
-These commands will build and install version 8.3.16 to
+These commands will build and install version 8.5.12 to
 $SWIPL_LOCATION:
 
 ```
-$ git clone --recursive -b V8.3.19 --depth 1 https://github.com/swi-prolog/swipl-devel
+$ git clone --recursive -b V8.5.12 --depth 1 https://github.com/swi-prolog/swipl-devel
 $ cd swipl-devel
 $ mkdir build
 $ cd build

libpharos/CMakeLists.txt

@@ -39,6 +39,7 @@ set(PHAROS_SOURCES
   pdg.cpp
   prolog.cpp
   prologimpl.cpp
+  prolog_symexp.cpp
   revision.cpp
   riscops.cpp
   semantics.cpp
@@ -65,7 +66,7 @@ set(PHAROS_SOURCES
   )
 
 # Packages needed by libpharos
-find_package(SWIPL "8.2.0" REQUIRED)
+find_package(SWIPL "8.3.16" REQUIRED)
 find_package(SQLite REQUIRED)
 set(CURSES_NEED_NCURSES true)
 find_package(Curses REQUIRED)

libpharos/defuse.cpp

@@ -806,35 +806,13 @@ DUAnalysis::fake_read(SgAsmX86Instruction* insn, const AbstractAccess& aa) const
   // This approach is a little lazy but I didn't want to have to write my own visitor class to
   // look for a specific subexpression.
 
-  // JSG updated this with Robb M's guideance on searching for a subexpression.
-  using VisitAction = Rose::BinaryAnalysis::SymbolicExpr::VisitAction;
-  using Visitor = Rose::BinaryAnalysis::SymbolicExpr::Visitor;
-
   TreeNodePtr read_tn = aa.value->get_expression();
 
-  // The visitor needed to search for the fake read (subexpression)
-  struct SubxVisitor : Visitor {
-    TreeNodePtr needle_;
-
-    SubxVisitor(const TreeNodePtr &needle) : needle_(needle) { }
-
-    VisitAction preVisit(const TreeNodePtr &expr) {
-      if (expr->isEquivalentTo(needle_)) {
-        return Rose::BinaryAnalysis::SymbolicExpr::TERMINATE;
-      }
-      return Rose::BinaryAnalysis::SymbolicExpr::CONTINUE;
-    }
-    VisitAction postVisit(const TreeNodePtr&) {
-      return Rose::BinaryAnalysis::SymbolicExpr::CONTINUE;
-    }
-  };
-
   for (const AbstractAccess& waa : get_writes(insn->get_address())) {
     TreeNodePtr write_tn = waa.value->get_expression();
-    SubxVisitor read_subx(read_tn);
 
     // search if this write includes the read. If it does, then it is not fake
-    if (write_tn->depthFirstTraversal(read_subx) == Rose::BinaryAnalysis::SymbolicExpr::TERMINATE) {
+    if (has_subexp (write_tn, read_tn)) {
       // The read was somewhere in the write, so the value was _truly_ read, and we've already
       // established that it was initialized by someone else, so it's not a truly uninitialized
       // read.
@@ -1291,7 +1269,7 @@ DUAnalysis::make_call_dependencies(SgAsmX86Instruction* insn, SymbolicStatePtr&
     // the parameter onto the stack before the call.  This code is a little bit incorrect in
     // that we're assuming that all four bytes have still been modified by the same instruction
     // as the first byte was.
-    SymbolicValuePtr mca = SymbolicValue::promote(memcell->get_address());
+    SymbolicValuePtr mca = SymbolicValue::promote(memcell->address());
 
     // Use rops->readMemory to read memory to read either 32 or 64 bits depending on the
     // architecture.  In truth, we have no idea how large the object being pointed to is and
@@ -1380,6 +1358,39 @@ void update_jump_targets(const DescriptorSet& ds, SgAsmInstruction* insn) {
   }
 }
 
+void DUAnalysis::guess_function_delta() {
+  // Because it's shorter than current_function...
+  FunctionDescriptor* fd = current_function;
+
+
+  for (CFGVertex vertex : fd->get_return_vertices()) {
+    const SgAsmBlock *block = convert_vertex_to_bblock(cfg, vertex);
+    // Find the return instruction.
+    const SgAsmStatementPtrList &insns = block->get_statementList();
+    assert(insns.size() > 0);
+    SgAsmX86Instruction *last = isSgAsmX86Instruction(insns[insns.size() - 1]);
+    if (last != NULL and last->get_kind() == x86_ret) {
+      // Get the number of bytes popped off the stack by the return instruction (not counting the
+      // return address).
+      SgAsmExpressionPtrList &ops = last->get_operandList()->get_operands();
+      if (ops.size() > 0) {
+        SgAsmIntegerValueExpression *val = isSgAsmIntegerValueExpression(ops[0]);
+        if (val != NULL) {
+          // This is the number on the RETN instruction and is also our expected stack delta.
+          int64_t retn_size  = val->get_absoluteValue();
+          SDEBUG << "Guessing that function " << fd->address_string() << " pops "
+                 << retn_size << " additional bytes off the stack." << LEND;
+          // Mak a StackDelta() obect and record it as _our_ stack delta.  This value will get
+          // used if the analyzed function is recursive and calls itself.
+          StackDelta guessed = StackDelta(retn_size, ConfidenceGuess);
+          fd->update_stack_delta(guessed);
+          return;
+        }
+      }
+    }
+  }
+}
+
 void DUAnalysis::update_function_delta() {
   // Because it's shorter than current_function...
   FunctionDescriptor* fd = current_function;
@@ -2196,6 +2207,11 @@ DUAnalysis::solve_flow_equation_iteratively()
   sp_tracker.update_delta(current_function->get_address(), StackDelta(0, ConfidenceCertain),
                           sd_failures);
 
+  // If this function is recursive, we need a better guess for our own stack delta than just
+  // zero.  Make that guess and store it in the stack delta tracker cache before starting
+  // anlaysis.
+  guess_function_delta();
+
   // Do most of the real work.  Visit each block in the control flow graph, possibly multiple
   // times, merging predecessor states, emulating each block, and updating state histories.
   rstatus = loop_over_cfg();

libpharos/defuse.hpp

@@ -259,6 +259,7 @@ class DUAnalysis {
   LimitCode evaluate_bblock(SgAsmBlock* bblock);
   void update_call_targets(SgAsmX86Instruction* insn, SymbolicRiscOperatorsPtr& ops);
   void update_function_delta();
+  void guess_function_delta();
   void make_call_dependencies(SgAsmX86Instruction* insn, SymbolicStatePtr& cstate);
 
   // Report debugging messages.  No analysis.

libpharos/descriptors.cpp

@@ -1,4 +1,4 @@
-// Copyright 2015-2021 Carnegie Mellon University.  See LICENSE file for terms.
+// Copyright 2015-2022 Carnegie Mellon University.  See LICENSE file for terms.
 
 #include <boost/graph/graph_traits.hpp>
 #include <boost/graph/adjacency_list.hpp>
@@ -270,7 +270,7 @@ void partition(const ProgOptVarMap & vm)
   auto file = pfile.native();
   if (!vm.count("serialize")) {
     auto filename = pfile.filename().native();
-    auto sername = filename + ".serialized";
+    auto sername = bf::path{filename + ".serialized"};
     auto vmcopy = vm;
     vmcopy.emplace("serialize"s,
                    boost::program_options::variable_value{boost::any{sername}, false});

libpharos/ir.cpp

@@ -1,4 +1,4 @@
-// Copyright 2015-2019, 2021 Carnegie Mellon University.  See LICENSE file for terms.
+// Copyright 2015-2022 Carnegie Mellon University.  See LICENSE file for terms.
 
 #include "ir.hpp"
 #include "util.hpp"
@@ -24,7 +24,7 @@ using namespace pharos;
 using namespace pharos::ir;
 
 namespace {
-namespace IRSemantics2 = Rose::BinaryAnalysis::InstructionSemantics2;
+namespace IRSemantics2 = Rose::BinaryAnalysis::InstructionSemantics;
 
 using SymValue = IRSemantics2::SymbolicSemantics::SValue;
 using SymValuePtr = IRSemantics2::SymbolicSemantics::SValuePtr;
@@ -54,13 +54,13 @@ using SymState = IRSemantics2::SymbolicSemantics::State;
 using SymStatePtr = IRSemantics2::SymbolicSemantics::StatePtr;
 using SymRiscOperators = IRSemantics2::SymbolicSemantics::RiscOperators;
 using SymRiscOperatorsPtr = IRSemantics2::SymbolicSemantics::RiscOperatorsPtr;
-using BaseDispatcher = Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::Dispatcher;
-using BaseDispatcherPtr = Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::DispatcherPtr;
+using BaseDispatcher = Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::Dispatcher;
+using BaseDispatcherPtr = Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::DispatcherPtr;
 
 using IRRegisterStatePtr = boost::shared_ptr<class IRRegisterState>;
 using IRRiscOperatorsPtr = boost::shared_ptr<class IRRiscOperators>;
 
-using SemanticsException = Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics::Exception;
+using SemanticsException = Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics::Exception;
 
 // Stub implementation
 bool is_register(Register r) {
@@ -1169,7 +1169,7 @@ Register IR::get_reg(RegisterDescriptor rd) const {
     GFATAL << "Unable to find register " << rd << LEND;
     exit(EXIT_FAILURE);
   }
-  Register exp = Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics::SValue::promote(reg_it->value)->get_expression()->isLeafNode();
+  Register exp = Rose::BinaryAnalysis::InstructionSemantics::SymbolicSemantics::SValue::promote(reg_it->value)->get_expression()->isLeafNode();
   assert (exp);
 
   return exp;

libpharos/ir.hpp

@@ -1,4 +1,4 @@
-// Copyright 2015-2021 Carnegie Mellon University.  See LICENSE file for terms.
+// Copyright 2015-2022 Carnegie Mellon University.  See LICENSE file for terms.
 
 #ifndef Pharos_Ir_H
 #define Pharos_Ir_H
@@ -20,7 +20,11 @@
 #include <boost/graph/graphviz.hpp>
 
 #include "rose.hpp"
+#if PHAROS_ROSE_SYMBOLIC_EXTENSION_HACK
+#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
+#else
 #include <Rose/BinaryAnalysis/InstructionSemantics2/SymbolicSemantics.h>
+#endif
 
 #include "calls.hpp"
 #include "cdg.hpp"
@@ -33,7 +37,7 @@ using CFG = Rose::BinaryAnalysis::ControlFlow::Graph;
 using CFGVertex = boost::graph_traits<CFG>::vertex_descriptor;
 
 namespace SymbolicExpr = Rose::BinaryAnalysis::SymbolicExpr;
-namespace BaseSemantics = Rose::BinaryAnalysis::InstructionSemantics2::BaseSemantics;
+namespace BaseSemantics = Rose::BinaryAnalysis::InstructionSemantics::BaseSemantics;
 using SymbolicExprPtr = SymbolicExpr::Ptr;
 using SymbolicLeaf = SymbolicExpr::Leaf;
 using SymbolicLeafPtr = SymbolicExpr::LeafPtr;

libpharos/method.cpp

@@ -538,9 +538,12 @@ bool ThisCallMethod::validate_vtable(ConstVirtualTableInstallationPtr install) {
     // embeds another object and the constuctor for the embeded object was inlined into
     // this method, we get misleading results here.
     if (!(vp->isEquivalentTo(leaf))) {
-      GDEBUG << "Rejected virtual function table write for wrong object " << *vp << " != "
-             << *leaf << " at instruction: " << debug_instruction(insn) << LEND;
-      return false;
+
+      // 2/16/22: ejs disabled this to see possibleVFTableWrites that were inlined
+
+      // GDEBUG << "Rejected virtual function table write for wrong object " << *vp << " != "
+      //        << *leaf << " at instruction: " << debug_instruction(insn) << LEND;
+      //return false;
     }
   }
 

libpharos/misc.cpp

@@ -1100,6 +1100,36 @@ template void debug_print_expression(
   std::ostream & stream, SymbolicSemantics::SValuePtr const & e);
 template void debug_print_expression(SymbolicSemantics::SValuePtr const & e);
 
+bool has_subexp (const TreeNodePtr haystack, const TreeNodePtr needle) {
+
+  using Rose::BinaryAnalysis::SymbolicExpr::VisitAction;
+  using Rose::BinaryAnalysis::SymbolicExpr::Visitor;
+  using Rose::BinaryAnalysis::SymbolicExpr::CONTINUE;
+  using Rose::BinaryAnalysis::SymbolicExpr::TERMINATE;
+
+  struct SubxVisitor : Visitor {
+    
+    TreeNodePtr needle_;
+
+    SubxVisitor(const TreeNodePtr &needle) : needle_(needle) {}
+
+    virtual VisitAction preVisit(const TreeNodePtr &expr) override {
+      if (expr->isEquivalentTo(needle_)) {
+        return TERMINATE;
+      }
+      return CONTINUE;
+    }
+    virtual VisitAction postVisit(const TreeNodePtr&) override {
+      return CONTINUE;
+    }
+  };
+
+  SubxVisitor read_subx(needle);
+
+  // search if this write includes the read. If it does, then it is not fake
+  return (haystack->depthFirstTraversal(read_subx) == Rose::BinaryAnalysis::SymbolicExpr::TERMINATE);
+}
+
 } // namespace pharos
 
 /* Local Variables:   */

libpharos/misc.hpp

@@ -1,4 +1,4 @@
-// Copyright 2015-2021 Carnegie Mellon University.  See LICENSE file for terms.
+// Copyright 2015-2022 Carnegie Mellon University.  See LICENSE file for terms.
 
 #ifndef Pharos_Misc_H
 #define Pharos_Misc_H
@@ -8,19 +8,29 @@
 #include "rose.hpp"
 // For TreeNodePtr, LeafNodePtr, etc.
 #include <Rose/BinaryAnalysis/SymbolicExpr.h>
-// For Semantics2 namespace.
+// For Semantics namespace.
+#if PHAROS_ROSE_SYMBOLIC_EXTENSION_HACK
+#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
+#else
 #include <Rose/BinaryAnalysis/InstructionSemantics2/SymbolicSemantics.h>
+#endif
 // For P2 namespace.
 #include <Rose/BinaryAnalysis/Partitioner2/Partitioner.h>
 #include <Rose/BinaryAnalysis/MemoryMap.h>
 
 #include <numeric>
 
+#if !PHAROS_ROSE_SYMBOLIC_EXTENSION_HACK
+namespace Rose{ namespace BinaryAnalysis {
+namespace InstructionSemantics = Rose::BinaryAnalysis::InstructionSemantics2;
+}}
+#endif
+
 namespace pharos {
 
 using Rose::BinaryAnalysis::MemoryMap;
 namespace P2 = Rose::BinaryAnalysis::Partitioner2;
-namespace Semantics2 = Rose::BinaryAnalysis::InstructionSemantics2;
+namespace Semantics2 = Rose::BinaryAnalysis::InstructionSemantics;
 namespace SymbolicSemantics = Semantics2::SymbolicSemantics;
 
 // Make sure overload resolution for operator<< can see into the global namespace
@@ -108,7 +118,7 @@ std::string addr_str(rose_addr_t addr);
 rose_addr_t address_from_node(LeafNodePtr tnp);
 
 // Make the ROSE Semantics2 namespace a little shorter to type...
-namespace Semantics2 = Rose::BinaryAnalysis::InstructionSemantics2;
+namespace Semantics2 = Rose::BinaryAnalysis::InstructionSemantics;
 
 // Expression printers (very useful from a debugger)
 void print_expression(std::ostream & stream, TreeNode & e);
@@ -178,6 +188,8 @@ using Rose::BinaryAnalysis::RegisterDictionary;
 
 void set_glog_name(std::string const & name);
 
+bool has_subexp (const TreeNodePtr haystack, const TreeNodePtr needle);
+
 } // namespace pharos
 
 // The main program need to provide a global logging facility.