Search Results

Documents authored by Cassez, Franck

Document
Invited Talk
DOI: 10.4230/OASIcs.FMBC.2024.1
Deductive Verification of Smart Contracts (Invited Talk)

Authors: Franck Cassez

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract
At the core of the Ethereum network is the Ethereum Virtual Machine (EVM) which can execute programs written in EVM bytecode. This remarkable feature empowers users to define complex business logic that can be executed programmatically by programs called smart contracts. Smart contracts are programs and may contain bugs. There are several examples of smart contract vulnerabilities that have been exploited in the past: in 2016, a re-entrance vulnerability in the Decentralised Autonomous Organisation (DAO) smart contract was exploited to steal more than USD50 Million. The total value netted from DeFi hacks in 2023 is estimated to be more than $1.5 billion. In this talk I will discuss formal verification of smart contracts. The main technique is deductive verification supported by the verification-friendly language Dafny. I will show how we can use deductive verification to reason about smart contracts, from high-level specifications (Dafny), to intermediate representation (Yul) and finally low-level EVM bytecode.
Cite as

Franck Cassez. Deductive Verification of Smart Contracts (Invited Talk). In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{cassez:OASIcs.FMBC.2024.1,
  author =	{Cassez, Franck},
  title =	{{Deductive Verification of Smart Contracts}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{1:1--1:1},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.1},
  URN =		{urn:nbn:de:0030-drops-198664},
  doi =		{10.4230/OASIcs.FMBC.2024.1},
  annote =	{Keywords: Smart Contracts, Deductive Verification}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.545
Summary-Based Inter-Procedural Analysis via Modular Trace Refinement

Authors: Franck Cassez, Christian Müller, and Karla Burnett

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We propose a generalisation of trace refinement for the verification of inter-procedural programs. Our method is a top-down modular, summary-based approach, and analyses inter-procedural programs by building function summaries on-demand and improving the summaries each time a function is analysed. Our method is sound, and complete relative to the existence of a modular Hoare proof for a non-recursive program. We have implemented a prototype analyser that demonstrates the main features of our approach and yields promising results.
Cite as

Franck Cassez, Christian Müller, and Karla Burnett. Summary-Based Inter-Procedural Analysis via Modular Trace Refinement. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 545-556, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{cassez_et_al:LIPIcs.FSTTCS.2014.545,
  author =	{Cassez, Franck and M\"{u}ller, Christian and Burnett, Karla},
  title =	{{Summary-Based Inter-Procedural Analysis via Modular Trace Refinement}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{545--556},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.545},
  URN =		{urn:nbn:de:0030-drops-48708},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.545},
  annote =	{Keywords: Program verification, Hoare Logic, Refinement, Automata}
}
Document
DOI: 10.4230/OASIcs.WCET.2012.1
What is a Timing Anomaly?

Authors: Franck Cassez, René Rydhof Hansen, and Mads Chr. Olesen

Published in: OASIcs, Volume 23, 12th International Workshop on Worst-Case Execution Time Analysis (2012)

Abstract
Timing anomalies make worst-case execution time analysis much harder, because the analysis will have to consider all local choices. It has been widely recognised that certain hardware features are timing anomalous, while others are not. However, defining formally what a timing anomaly is, has been difficult. We examine previous definitions of timing anomalies, and identify examples where they do not align with common observations. We then provide a definition for consistently slower hardware traces that can be used to define timing anomalies and aligns with common observations.
Cite as

Franck Cassez, René Rydhof Hansen, and Mads Chr. Olesen. What is a Timing Anomaly?. In 12th International Workshop on Worst-Case Execution Time Analysis. Open Access Series in Informatics (OASIcs), Volume 23, pp. 1-12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{cassez_et_al:OASIcs.WCET.2012.1,
  author =	{Cassez, Franck and Hansen, Ren\'{e} Rydhof and Olesen, Mads Chr.},
  title =	{{What is a Timing Anomaly?}},
  booktitle =	{12th International Workshop on Worst-Case Execution Time Analysis},
  pages =	{1--12},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-41-5},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{23},
  editor =	{Vardanega, Tullio},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.WCET.2012.1},
  URN =		{urn:nbn:de:0030-drops-35521},
  doi =		{10.4230/OASIcs.WCET.2012.1},
  annote =	{Keywords: Timing anomalies, worst case execution time (WCET), abstractions}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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