Static and Symbolic Analysis

March 15, 2019

Static Analysis

Static analysis can be described as a way to test code without actually executing it. The idea here is to use a computer program to analyse a program’s source code without running it.

Static analysis has a few sub components such as Flow Analysis. This tracks how values might flow between the different memory relocations in a program. Tainted Flow Analysis is often referred to where untrusted input is considered tainted, eg input from a user and conversely, hardcoded values or constants are untainted.

Flow Analysis can have “sensitivity” added to increase the precision and also to reduce false positives. It basically accounts for variables whose contents change, typically by using extra qualifiers.

Context Sensitivity Analysis is another sub component of Static Analysis where calling other functions can cause false positives. “So context sensitive analysis solves this problem by distinguishing call sites in some way, so that we don’t allow a call at one place to return it’s value to another call.”

Symbolic Analysis

Symbolic execution aims to generalise testing so that instead of testing with actual values, tests are run with variables. The image below explains it best.

Concolic testing is another term often thrown in when discussing symbolic execution or symbolic analysis. The word concolic is a portmanteau of concrete and symbolic and is a hybrid software verification technique that performs symbolic execution, a classical technique that treats program variables as symbolic variables, along a concrete execution (testing on particular inputs) path.

For more information, check out this Coursera course on Software Security

What does this have to do with Blockchain? The main language of smart contracts in Ethereum is Solidity and the language is still relatively immature. There are a bunch of code analysers though to help find bugs in your smart contracts. The options are as follows:

  • Echidna
    • A fuzzer on EVM that also takes Solidity input
    • Able to fuzz a program with sequences of multiple transactions
    • An automatic tool that detects trace vulnerabilities (Greedy, Prodigal and Suicidal) with depth-first search of symbolic execution of multiple invocations
  • Mythril
    • A blockchain exploration tool that indexes all contracts on the network, containing a disassembler, an ABI function detector and a control flow analyzer
    • Comes with a –fire-laser option
    • Powered by laser-ethereum
  • porosity
    • A reverse enginering tool, a disassembler, an ABI function detector and a decompiler that also highlights vulnerabilities
  • Manticore
    • A symbolic execution engine that can generate inputs to cover codepaths (asciicast), which also comes with a Python API
  • evmdis
    • A disassembler for EVM code
  • ethersplay
  • Securify
    • A tool that strives to achieve no false-negatives
    • The implementation seems not public as of now
  • Oyente
    • An automatic EVM code analyzer based on symbolic execution and Z3 SMT solver
  • Dr. Y’s Ethereum Contract Analyzer
    • A symbolic executor for EVM code


Leave a Comment!

Your email address will not be published.