Project funded by the Vienna Science and Technology Fund

Duration: 2023-09-01 ‒ 2027-08-31 (ongoing)

Funding: € 7999.900

Members

• Dr.in. sc. Maria Christakis (PI), Professor, TU Wien

• Christoph Hochrainer, Dipl. Ing., Pre-doc, TU Wien

• Dr. Matteo Maffei (co-PI), Professor, TU Wien

• Markus Scherer , MSc, Pre-doc, TU Wien

• Dr.in. techn. Laura Kovács (co-PI), Professor, TU Wien

• Johannes Schoisswohl, Dipl.-Ing. / BSc, Pre-doc, TU Wien

• Sophie Rain, Dipl.-Ing.in / BSc, Pre-doc, TU Wien

• Clemens Eisenhofer, Dipl.-Ing. / BSc, Pre-doc, TU Wien

• Robin Coutelier, MSc, Pre-doc, TU Wien

Project

Correctness and security of smart contracts is critical as digital assets may be at stake. To detect or evenis critical as digital assets may be at stake. To detect or even avoid such vulnerabilities in smart contracts, there have emerged bug-finding techniques, which lackin smart contracts, there have emerged bug-finding techniques, which lack soundness, and verification techniques, which lack precision.

In ForSmart, we aim to develop a hybrid, automated certification framework for smart contracts thatIn ForSmart, we aim to develop a hybrid, automated certification framework for smart contracts that symbiotically combines bug-finding in the form of test generation and verification in the form of sound staticin the form of test generation and verification in the form of sound static analysis, thereby achieving soundness and precision. Advanced automated-reasoning mechanisms, which we plan to develop and tailor to this domain, will support both testing and static analysis.to this domain, will support both testing and static analysis.

We will maximize the impact of ForSmart by applying our framework to concrete applications of academic,of academic, industrial, and public relevance, such as DeFi apps, with a focus on certifying functional and securitya focus on certifying functional and security properties, as well as by making our infrastructure available to contract developers, auditors, and users. Weas by making our infrastructure available to contract developers, auditors, and users. We additionally plan to leverage our ongoing collaborations with Certora, the Ethereum Foundation, ConsenSys, and Microsoft Research.

We request funding for 3 PhD students. The duration of each PhD will be 4 years – the funding will cover3 PhD students. The duration of each PhD will be 4 years the funding will cover 3.5 years, and the remaining time will be spent on internships at the aforementioned companies tothe aforementioned companies to encourage industrial adoption of our framework.our framework.

The core team of ForSmart (PIs) has a 2/3 female participation. We aim to maintain such a balance when(Pls) has a 2/3 female participation. We aim to maintain such a balance when expanding

Keywords: test generation, static analysis, automated reasoning, hybrid, certification, smart contracts

Results

• -Jana Chadt, Christoph Hochrainer, Valentin Wüstholz and Maria Christakis. Olympia: Fuzzer Benchmarking for Solidity. In Proceedings of the 39th International Conference on Automated Software Engineering (ASE'24), 2024. ACM. https://mariachris.github.io/publications.html
• Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz and Arie Gurfinkel. Inductive Predicate Synthesis Modulo Programs. In Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP'24), 2024. Schloss Dagstuhl. https://mariachris.github.io/Pubs/ECOOP-2024.pdf
• Johannes Schoisswohl, Laura Kovács, Konstantin Korovin. VIRAS: Conflict-Driven Quantifier Elimination for Integer-Real Arithmetic. LPAR 2024: 147-164
• Pamina Georgiou, Márton Hajdú, Laura Kovács. Saturating Sorting without Sorts. LPAR 2024: 88-105. https://easychair.org/publications/paper/qbDc
• Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel, Laura Kovács, Michael Rawson. Scaling CheckMate for Game-Theoretic Security. LPAR 2024: 222-231. https://easychair.org/publications/paper/6ZDH
• Márton Hajdú, Laura Kovács, Michael Rawson. Rewriting and Inductive Reasoning. LPAR 2024: 278-294. https://easychair.org/publications/paper/T1mjX
• S. Jeanteur, L. Kovacs, M. Maffei and M. Rawson, “CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model,” in 2024 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, USA, 2024 pp. 3165-3183. https://doi.org/10.1109/SP54263.2024.00246
• Clemens Eisenhofer, Laura Kovács, Michael Rawson. Embedding the Connection Calculus in Satisfiability Modulo Theories. AReCCa@TABLEAUX 2023: 54-63. https://ceur-ws.org/Vol-3613/AReCCa2023_paper4.pdf
• Laura Kovács, Petra Hozzová, Marton Hajdu, Andrei Voronkov. Induction in Saturation. IJCAR 2024: 21-29. https://doi.org/10.1007/978-3-031-63498-7_2
• Márton Hajdu, Laura Kovács, Michael Rawson, Andrei Voronkov. Reducibility Constraints in Superposition. IJCAR 2024: 115-132. https://doi.org/10.1007/978-3-031-63498-7_8
• Petra Hozzová, Daneshvar Amrollahi, Márton Hajdu, Laura Kovács, Andrei Voronkov, Eva Maria Wagner. Synthesis of Recursive Programs in Saturation. IJCAR 2024: 154-171. https://doi.org/10.1007/978-3-031-63498-7_10
• Thomas Hader, Daniela Kaufmann, Ahmed Irfan, Stéphane Graham-Lengrand, Laura Kovács. MCSat-Based Finite Field Reasoning in the Yices2 SMT Solver (Short Paper). IJCAR 2024: 386–395. https://doi.org/10.1007/978-3-031-63498-7_23