Read the KLEE paper

  1. Approaches used for improving software reliability:
    • Manual testing (Coverage + Known bugs):
      • No guarantees (no amount of testing can guarantee that you're free of bugs)
      • High Manual Effort
      • Limitation of human thought
    • Coding standards
    • Code Review
    • Tool Support
  2. Classifying bugs:
    • General / Genetic bugs:
      • Division or modulo by 0
      • Assertion failure
      • Integer overflow
      • Invalid dynamic cast
    • Memory bugs:
      • Out-of-bounds array access
      • Double free, access after free
      • Dereferencing a null pointer
    • Concurrency bugs:
      • Deadlock
      • Data Races
    • Termination bugs:
      • Infinite loop
      • Unbounded recursion (in a non lazily evaluated language)
    • Functional bugs:
      • Logic error / Incorrect implementation of the algorithm
  3. Safety Properties:
    • Can be expressed using assertions and program instrumentation
    • No null dereferences -- insert assertion before each dereference
    • No out-of-bounds access -- assertions
    • No division by zero -- assertions
    • Initialisation, processing and destruction can only be called in sequence
  4. Dynamic Analysis:
    • Advantages:
      • Precise (only observes what the program can actually do)
      • Scalable (in many cases proportional to regular execution)
    • Disadvantages:
      • Requires the whole SUT
      • Requires the execution environment or a simulator
      • Usefulness is determined by the test inputs
    • Examples:
  5. Static Analysis:
    • Advantages:
      • Can detect defects not revealed by existing test cases
      • High coverage: Can potentially prove properties about a large number of possible executions
      • Can be applied to incomplete systems (start early)
      • Highly scalable if applied in a modular fashion
    • Disadvantages:
      • Can be precise, but extremely expensive (cover all possible executions)
      • Can be fast, but extremely imprecise (lots of false positives)
    • Examples:
      • Compilers (warnings)
      • Safe C Compilers
      • Linters (enforce code quality in hope of reducing bugs)
      • Internal tools (e.g. Microsoft's Static Driver Verifier)
  6. Types of errors:
    • False positives:
      • Warning about a problem that cannot actually occur
      • Analysis is said to be imprecise if it reports a large number of false positives
      • Analysis that may report false positives is said to be incomplete
      • Hinder the use of analysis tools in day-to-day usage
    • False Negatives:
      • No warnings reported, while there exists an issue
      • Analyser is called unsound if it reports false negatives
      • Bad when analysing safety critical software
  7. Towards Optimisation-Safe Systems: Analysing the Impact of UB
  8. Data Flow Analysis:
    • Derives information about the flow of data along program execution paths
    • Analysis is done in the abstract domain, related to abstract interpretation
    • Data flow analysis framework consists of:
      • A direction of the data flow (forwards or backwards)
      • A family of transfer functions
      • A meet operator