Benjamin Mariano

selected publications

1. OOPSLA’22

   Automated Transpilation of Imperative to Functional Code Using Neural-Guided Program Synthesis

   Mariano, Benjamin, Chen, Yanju, Feng, Yu, Durrett, Greg,  and Dillig, Işil

   Proc. ACM Program. Lang. Apr 2022

   Abs arXiv Bib PDF

   While many mainstream languages such as Java, Python, and C# increasingly incorporate functional APIs to simplify programming and improve parallelization/performance, there are no effective techniques that can be used to automatically translate existing imperative code to functional variants using these APIs. Motivated by this problem, this paper presents a transpilation approach based on inductive program synthesis for modernizing existing code. Our method is based on the observation that the overwhelming majority of source/target programs in this setting satisfy an assumption that we call trace-compatibility: not only do the programs share syntactically identical low-level expressions, but these expressions also take the same values in corresponding execution traces. Our method leverages this observation to design a new neural-guided synthesis algorithm that (1) uses a novel neural architecture called cognate grammar network (CGN) and (2) leverages a form of concolic execution to prune partial programs based on intermediate values that arise during a computation. We have implemented our approach in a tool called NGST2 and use it to translate imperative Java and Python code to functional variants that use the Stream and functools APIs respectively. Our experiments show that NGST2 significantly outperforms several baselines and that our proposed neural architecture and pruning techniques are vital for achieving good results.

   @article{mariano2022transpilation,
     author = {Mariano, Benjamin and Chen, Yanju and Feng, Yu and Durrett, Greg and Dillig, I\c{s}il},
     title = {Automated Transpilation of Imperative to Functional Code Using Neural-Guided Program Synthesis},
     year = {2022},
     issue_date = {April 2022},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     volume = {6},
     number = {OOPSLA1},
     url = {https://doi.org/10.1145/3527315},
     doi = {10.1145/3527315},
     journal = {Proc. ACM Program. Lang.},
     month = apr,
     articleno = {71},
     numpages = {27},
     keywords = {transpilation, neural networks, program synthesis},
   }

2. POPL’22

   SolType: Refinement Types for Arithmetic Overflow in Solidity.

   Tan, Bryan,  Mariano, Benjamin, Lahiri, Shuvendu K., Dillig, Işil,  and Feng, Yu

   Proc. ACM Program. Lang. Apr 2022

   Abs Bib PDF

   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

   @article{tan2022soltype,
     title = {SolType: Refinement Types for Arithmetic Overflow in Solidity.},
     author = {Tan, Bryan and Mariano, Benjamin and Lahiri, Shuvendu K. and Dillig, I\c{s}il and Feng, Yu},
     journal = {Proc. ACM Program. Lang.},
     volume = {6},
     number = {POPL},
     pages = {1--29},
     year = {2022},
   }

3. S&P’21

   SmartPulse: Automated Checking of Temporal Properties in Smart Contracts

   Stephens, Jon, Ferles, Kostas,  Mariano, Benjamin, Lahiri, Shuvendu K.,  and Dillig, Işil

   In 2021 IEEE Symposium on Security and Privacy (SP) Apr 2021

   Abs Bib PDF

   Smart contracts are programs that run on the blockchain and digitally enforce the execution of contracts between parties. Because bugs in smart contracts can have serious monetary consequences, ensuring the correctness of such software is of utmost importance. In this paper, we present a novel technique, and its implementation in a tool called SmartPulse, for automatically verifying temporal properties in smart contracts. SmartPulse is the first smart contract verification tool that is capable of checking liveness properties, which ensure that “something good” will eventually happen (e.g., “I will eventually receive my refund”). We experimentally evaluate SmartPulse on a broad class of smart contracts and properties and show that (a) SmartPulse allows automatically verifying important liveness properties, (b) it is competitive with or better than state-of-the-art tools for safety verification, and (c) it can automatically generate attacks for vulnerable contracts.

   @inproceedings{stephens2021smartpulse,
     author = {Stephens, Jon and Ferles, Kostas and Mariano, Benjamin and Lahiri, Shuvendu K. and Dillig, I\c{s}il},
     booktitle = {2021 IEEE Symposium on Security and Privacy (SP)},
     title = {SmartPulse: Automated Checking of Temporal Properties in Smart Contracts},
     year = {2021},
     volume = {},
     number = {},
     pages = {555-571},
     doi = {10.1109/SP40001.2021.00085},
   }

4. ASE’20

   Demystifying Loops in Smart Contracts

   Mariano, Benjamin, Chen, Yanju, Feng, Yu, Lahiri, Shuvendu K.,  and Dillig, Işil

   In 2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE) Apr 2020

   Abs Bib PDF

   This paper aims to shed light on how loops are used in smart contracts. Towards this goal, we study various syntactic and semantic characteristics of loops used in over 20,000 Solidity contracts deployed on the Ethereum blockchain, with the goal of informing future research on program analysis for smart contracts. Based on our findings, we propose a small domain-specific language (DSL) that can be used to summarize common looping patterns in Solidity. To evaluate what percentage of smart contract loops can be expressed in our proposed DSL, we also design and implement a program synthesis toolchain called Solis that can synthesize loop summaries in our DSL. Our evaluation shows that at least 56% of the analyzed loops can be summarized in our DSL, and 81% of these summaries are exactly equivalent to the original loop.

   @inproceedings{mariano2020demystifying,
     author = {Mariano, Benjamin and Chen, Yanju and Feng, Yu and Lahiri, Shuvendu K. and Dillig, I\c{s}il},
     booktitle = {2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE)},
     title = {Demystifying Loops in Smart Contracts},
     year = {2020},
     volume = {},
     number = {},
     pages = {262-274},
     doi = {},
   }