SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Sat 10 Dec 2022 14:30 - 15:00 at Seminar Room LG004 - PLDI and POPL Papers Chair(s): Joxan Jaffar

As smart contracts gain adoption in financial transactions, it becomes increasingly important to ensure that they are free of bugs and security vulnerabilities. Of particular relevance in this context are arithmetic overflow bugs, as integers are often used to represent financial assets like account balances. Motivated by this observation, this paper presents SolType, a refinement type system for Solidity that can be used to prevent arithmetic over- and under-flows in smart contracts. SolType allows developers to add refinement type annotations and uses them to prove that arithmetic operations do not lead to over- and under-flows. SolType incorporates a rich vocabulary of refinement terms that allow expressing relationships between integer values and aggregate properties of complex data structures. Furthermore, our implementation, called Solid, incorporates a type inference engine and can automatically infer useful type annotations, including non-trivial contract invariants.

To evaluate the usefulness of our type system, we use Solid to prove arithmetic safety of a total of 120 smart contracts. When used in its fully automated mode (i.e., using Solid’s type inference capabilities), Solid is able to eliminate 86.3% of redundant runtime checks used to guard against overflows. We also compare Solid against a state-of-the-art arithmetic safety verifier called VeriSmart and show that Solid has a significantly lower false positive rate, while being significantly faster in terms of verification time.

Sat 10 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
PLDI and POPL PapersCOVID Time Papers In Person at Seminar Room LG004
Chair(s): Joxan Jaffar National University of Singapore
13:30
30m
Talk
PMEvo: portable inference of port mappings for out-of-order processors by evolutionary optimization
COVID Time Papers In Person
Fabian Ritter Saarland University, Germany, Sebastian Hack Saarland University, Germany
Link to publication DOI
14:00
30m
Talk
Software Model-Checking as Cyclic-Proof Search
COVID Time Papers In Person
Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP
Link to publication DOI
14:30
30m
Talk
SolType: Refinement Types for Arithmetic Overflow in Solidity
COVID Time Papers In Person
Bryan Tan , Benjamin Mariano The University of Texas at Austin, Texas, USA, Shuvendu Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara
Link to publication DOI