Solidity

• 🟩: Easy to implement
• 🟧: Medium
• 🟥: Hard
• ⚠️: Important, highest priority. Because they are commonly seen in real-world smart contracts.
• ❔: Not sure
• AA: Supported

Frontend Construction

TODO List

• Type
  • Rational Literals 🟩
  • User-defined Value Types 🟧
    • Almost identical to alias or typedef.
  • Mapping 🟥⚠️
    • Can also be valuable for C++/Python frontend.
  • Function Types Members❔
    • .address 🟩⚠️
    • .selector ❔
• Events❔⚠️
  • I would say it is 🟩, because it does not really affect the verification, only outputting logs. Maybe just parse it and do nothing
• Errors🟩⚠️
  • ❔Do we need to implement roll back❔
• Units and Globally Available Variables
  • Ether Units 🟧
  • Time Units 🟧
    • Maybe 🟩. I am just not sure what they should be converted to.
  • Block and Transaction Properties 🟩⚠️
    • Can be regarded as built-in variables which should be preloaded before parsing (?)
    • the value of these built-in properties should be non-deterministic. However, might construct an interface to allow user-defined value in the future.
  • ABI Encoding and Decoding Functions 🟧⚠️
  • Members of bytes 🟥
    • byte.concat
    • byte.length
    • byte.push
    • byte.pop ⚠️ Very important. There is a type of vulnerability called popping an empty array. (0x31)
  • Members of string 🟩
    • string.concat: convert to c:@F@strncat
  • Mathematical and Cryptographic Functions 🟧⚠️
  • Members of Address Types ❔⚠️
  • Contract-related ❔⚠️
  • Type Information ❔
• Function
  • Function Calls with Named Parameters 🟩
  • Destructuring Assignments and Returning Multiple Values 🟥⚠️
    • Basically, tuple in python
    • Can also be valuable for C++/Python frontend.
  • Omitted Names in Function Definitions 🟥
  • Scoping and Declarations 🟩⚠️
  • Call a zero-initialized variable of internal function type ⚠️
    • Another vulnerability type (0x51)
• Function Modifiers 🟧
• Interface ❔⚠️
• Abstract ❔⚠️
• Keywords
  • delete
  • super
  • this
  • …

Known Bugs

• Inheritance. Completely broken.
  • The override and virtual still contain bugs.
• Incomplete message output related to struct. (e.g. Assertion struct.id == 1 failed is reported as struct. == 1)
• out-of-bounds Bytes (0x32) 🟧⚠️
• (need investigation) We did not implement the rollback features in Solidity. Will it affect the verification result?

Resource List

• cprover: Background Concepts
• ESBMC-solidity: an SMT-based model checker for solidity smart contracts
• ESBMC Document
• solidity/docs at develop · ethereum/solidity

Solidity Error Code

0x01: If you call assert with an argument that evaluates to false.
0x11: If an arithmetic operation results in underflow or overflow outside of an unchecked { ... } block.
0x12: If you divide or modulo by zero (e.g. 5 / 0 or 23 % 0).
0x21: If you convert a value that is too big or negative into an enum type.
0x31: If you call .pop() on an empty array.
0x32: If you access an array, bytesN or an array slice at an out-of-bounds or negative index (i.e. x[i] where i >= x.length or i < 0).
0x41: If you allocate too much memory or create an array that is too large.
0x51: If you call a zero-initialized variable of internal function type