Agenda

11 May 2026 12:00

Language-based security in smart contract platforms:semantic foundations and cross-chain compilation

Aula EPSILON 2 - Edificio EPSILON | Campus Scientifico

Speaker:
Lorenzo Benetollo, Università Ca' Foscari Venezia e Università di Camerino

Abstract:
Smart contract platforms have become core infrastructures for decentralized applications, securing an ecosystem worth over 3.5 trillion USD. As these contracts increasingly govern financial value, trust, and decision-making, the design of their programming languages plays a crucial role in system security. This thesis investigates how language design and secure compilation can improve the reliability of smart contracts across heterogeneous blockchain platforms. It first presents a comparative analysis of smart contract languages, showing how design choices in type systems, storage models, and execution semantics directly affect vulnerability surfaces. Building on this analysis, the thesis introduces AlgoMove, a framework that brings Move’s resource-oriented programming model to Algorand through semantics-preserving compilation to TEAL. It then presents Move2EVM, which extends Move-to-EVM compilation with an inlined reference monitor to enforce Move’s safety guarantees at runtime with modest gas overhead. Finally, the thesis addresses reentrancy in Solidity by providing a formal characterization based on Non-Interference and by evaluating current detection tools against a benchmark of 134 validated real-world vulnerabilities. The results show that existing tools systematically miss important cases, highlighting the need for more semantics-aware analysis. Overall, the thesis demonstrates that principled language design and secure compilation are key to improving blockchain security in a high-value, high-risk ecosystem.

Bio sketch:
Lorenzo Benetollo is a PhD candidate in the Italian National PhD Program on Blockchain and Distributed Ledger Technology, specialized in programming languages and smart contract security. His research focuses on secure compilation techniques for blockchain platforms, with particular attention to preserving language-level safety guarantees across different virtual machines. During his PhD, he worked on projects such as AlgoMove and Move-to-EVM, investigating how the Move programming language can be compiled to targets such as Algorand’s TEAL approval language and Ethereum Virtual Machine bytecode while maintaining strong security properties. His work combines language-based security, compiler design, and formal methods. He is currently an Applied Research Engineer at the IOTA Foundation, where he contributes to the development and maintenance of the Move on IOTA programming language and its smart contract infrastructure. More broadly, his research interests lie in the design and implementation of safer and more reliable smart contract programming languages, bridging the gap between high-level abstractions and low-level execution environments.

Language

The event will be held in English

Organized by

Sabina Rossi

Search in the agenda