4 Search Results for "Cecchetti, Ethan"

Document
DOI: 10.4230/OASIcs.FMBC.2025.3
Formal Verification in Solidity and Move: Insights from a Comparative Analysis

Authors: Massimo Bartoletti, Silvia Crafa, and Enrico Lipparini

Published in: OASIcs, Volume 129, 6th International Workshop on Formal Methods for Blockchains (FMBC 2025)

Abstract
Formal verification plays a crucial role in making smart contracts safer, being able to find bugs or to guarantee their absence, as well as checking whether the business logic is correctly implemented. For Solidity, even though there already exist several mature verification tools, the semantical quirks of the language can make verification quite hard in practice. Move, on the other hand, has been designed with security and verification in mind, and it has been accompanied since its early stages by a formal verification tool, the Move Prover. In this paper, we investigate through a comparative analysis: 1) how the different designs of the two contract languages impact verification, and 2) what is the state-of-the-art of verification tools for the two languages, and how do they compare on three paradigmatic use cases. Our investigation is supported by an open dataset of verification tasks performed in Certora and in the Aptos Move Prover.
Cite as

Massimo Bartoletti, Silvia Crafa, and Enrico Lipparini. Formal Verification in Solidity and Move: Insights from a Comparative Analysis. In 6th International Workshop on Formal Methods for Blockchains (FMBC 2025). Open Access Series in Informatics (OASIcs), Volume 129, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bartoletti_et_al:OASIcs.FMBC.2025.3,
  author =	{Bartoletti, Massimo and Crafa, Silvia and Lipparini, Enrico},
  title =	{{Formal Verification in Solidity and Move: Insights from a Comparative Analysis}},
  booktitle =	{6th International Workshop on Formal Methods for Blockchains (FMBC 2025)},
  pages =	{3:1--3:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-371-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{129},
  editor =	{Marmsoler, Diego and Xu, Meng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2025.3},
  URN =		{urn:nbn:de:0030-drops-230302},
  doi =		{10.4230/OASIcs.FMBC.2025.3},
  annote =	{Keywords: Smart contracts, Solidity, Move, Verification, Blockchain}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2025.25
Optimal Oblivious Algorithms for Multi-Way Joins

Authors: Xiao Hu and Zhiang Wu

Published in: LIPIcs, Volume 328, 28th International Conference on Database Theory (ICDT 2025)

Abstract
In cloud databases, cloud computation over sensitive data uploaded by clients inevitably causes concern about data security and privacy. Even if cryptographic primitives and trusted computing environments are integrated into query processing to safeguard the actual contents of the data, access patterns of algorithms can still leak private information about data. Oblivious RAM (ORAM) and circuits are two generic approaches to address this issue, ensuring that access patterns of algorithms remain oblivious to the data. However, deploying these methods on insecure algorithms, particularly for multi-way join processing, is computationally expensive and inherently challenging. In this paper, we propose a novel sorting-based algorithm for multi-way join processing that operates without relying on ORAM simulations or other security assumptions. Our algorithm is a non-trivial, provably oblivious composition of basic primitives, with time complexity matching the insecure worst-case optimal join algorithm, up to a logarithmic factor. Furthermore, it is cache-agnostic, with cache complexity matching the insecure lower bound, also up to a logarithmic factor. This clean and straightforward approach has the potential to be extended to other security settings and implemented in practical database systems.
Cite as

Xiao Hu and Zhiang Wu. Optimal Oblivious Algorithms for Multi-Way Joins. In 28th International Conference on Database Theory (ICDT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 328, pp. 25:1-25:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hu_et_al:LIPIcs.ICDT.2025.25,
  author =	{Hu, Xiao and Wu, Zhiang},
  title =	{{Optimal Oblivious Algorithms for Multi-Way Joins}},
  booktitle =	{28th International Conference on Database Theory (ICDT 2025)},
  pages =	{25:1--25:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-364-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{328},
  editor =	{Roy, Sudeepa and Kara, Ahmet},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2025.25},
  URN =		{urn:nbn:de:0030-drops-229662},
  doi =		{10.4230/LIPIcs.ICDT.2025.25},
  annote =	{Keywords: oblivious algorithms, multi-way joins, worst-case optimality}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.29
Semantics for Noninterference with Interaction Trees

Authors: Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Noninterference is the strong information-security property that a program does not leak secrets through publicly-visible behavior. In the presence of effects such as nontermination, state, and exceptions, reasoning about noninterference quickly becomes subtle. We advocate using interaction trees (ITrees) to provide compositional mechanized proofs of noninterference for multi-language, effectful, nonterminating programs, while retaining executability of the semantics. We develop important foundations for security analysis with ITrees: two indistinguishability relations, leading to two standard notions of noninterference with adversaries of different strength, along with metatheory libraries for reasoning about each. We demonstrate the utility of our results using a simple imperative language with embedded assembly, along with a compiler into that assembly language.
Cite as

Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. Semantics for Noninterference with Interaction Trees. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 29:1-29:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{silver_et_al:LIPIcs.ECOOP.2023.29,
  author =	{Silver, Lucas and He, Paul and Cecchetti, Ethan and Hirsch, Andrew K. and Zdancewic, Steve},
  title =	{{Semantics for Noninterference with Interaction Trees}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{29:1--29:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.29},
  URN =		{urn:nbn:de:0030-drops-182227},
  doi =		{10.4230/LIPIcs.ECOOP.2023.29},
  annote =	{Keywords: verification, information-flow, denotational semantics, monads}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.6
Semantics for Noninterference with Interaction Trees (Artifact)

Authors: Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Noninterference is the strong information-security property that a program does not leak secrets through publicly-visible behavior. In the presence of effects such as nontermination, state, and exceptions, reasoning about noninterference quickly becomes subtle. We advocate using interaction trees (ITrees) to provide compositional mechanized proofs of noninterference for multi-language, effectful, nonterminating programs, while retaining executability of the semantics. We develop important foundations for security analysis with ITrees: two indistinguishability relations, leading to two standard notions of noninterference with adversaries of different strength, along with metatheory libraries for reasoning about each. We demonstrate the utility of our results using a simple imperative language with embedded assembly, along with a compiler into that assembly language.
Cite as

Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, and Steve Zdancewic. Semantics for Noninterference with Interaction Trees (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 6:1-6:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{silver_et_al:DARTS.9.2.6,
  author =	{Silver, Lucas and He, Paul and Cecchetti, Ethan and Hirsch, Andrew K. and Zdancewic, Steve},
  title =	{{Semantics for Noninterference with Interaction Trees (Artifact)}},
  pages =	{6:1--6:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Silver, Lucas and He, Paul and Cecchetti, Ethan and Hirsch, Andrew K. and Zdancewic, Steve},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.6},
  URN =		{urn:nbn:de:0030-drops-182465},
  doi =		{10.4230/DARTS.9.2.6},
  annote =	{Keywords: verification, information-flow, denotational semantics, monads}
}
  • Refine by Type
  • 4 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 2 2025
  • 2 2023

  • Refine by Author
  • 2 Cecchetti, Ethan
  • 2 He, Paul
  • 2 Hirsch, Andrew K.
  • 2 Silver, Lucas
  • 2 Zdancewic, Steve
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 OASIcs
  • 1 DARTS

  • Refine by Classification
  • 2 Security and privacy → Information flow control
  • 2 Security and privacy → Logic and verification
  • 2 Theory of computation → Denotational semantics
  • 1 Information systems → Join algorithms
  • 1 Security and privacy → Management and querying of encrypted data
  • Show More...

  • Refine by Keyword
  • 2 denotational semantics
  • 2 information-flow
  • 2 monads
  • 2 verification
  • 1 Blockchain
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact