A program that maintains key safety properties even when interacting with arbitrary untrusted code is said to enjoy robust safety. Proving that a program written in a mainstream language is robustly safe is typically challenging because it requires static verification tools that work precisely even in the presence of language features like dynamic dispatch and shared mutability. The emerging Move programming language was designed to support strong encapsulation and static verification in the service of secure smart contract programming. However, the language design has not been analysed using a theoretical framework like robust safety.In this paper, we define robust safety for the Move language and introduce a generic framework for static tools that wish to enforce it. Our framework consists of two abstract components: a program verifier that can prove an invariant holds in a closedworld setting (e.g., the Move Prover [16, 47]), and a novel encapsulator that checks if the verifier's result generalizes to an open-world setting. We formalise an escape analysis as an instantiation of the encapsulator and prove that it attains the required security properties.Finally, we implement our encapsulator as an extension to the Move Prover and use the combination to analyse a large representative benchmark set of real-world Move programs. This toolchain certifies >99% of the Move modules we analyse, validating that automatic enforcement of strong security properties like robust safety is practical for Move. Additionally, our results tell that security-centric language design can be effective in attaining strong security properties such as robust safety.

Robust Safety for Move / Patrignani, M; Blackshear, S. - STAMPA. - (2023), pp. 308-323. (Intervento presentato al convegno csf tenutosi a Dubrovnik, Croatia nel 10-14 July 2023) [10.1109/CSF57540.2023.00045].

Robust Safety for Move

Patrignani, M;
2023-01-01

Abstract

A program that maintains key safety properties even when interacting with arbitrary untrusted code is said to enjoy robust safety. Proving that a program written in a mainstream language is robustly safe is typically challenging because it requires static verification tools that work precisely even in the presence of language features like dynamic dispatch and shared mutability. The emerging Move programming language was designed to support strong encapsulation and static verification in the service of secure smart contract programming. However, the language design has not been analysed using a theoretical framework like robust safety.In this paper, we define robust safety for the Move language and introduce a generic framework for static tools that wish to enforce it. Our framework consists of two abstract components: a program verifier that can prove an invariant holds in a closedworld setting (e.g., the Move Prover [16, 47]), and a novel encapsulator that checks if the verifier's result generalizes to an open-world setting. We formalise an escape analysis as an instantiation of the encapsulator and prove that it attains the required security properties.Finally, we implement our encapsulator as an extension to the Move Prover and use the combination to analyse a large representative benchmark set of real-world Move programs. This toolchain certifies >99% of the Move modules we analyse, validating that automatic enforcement of strong security properties like robust safety is practical for Move. Additionally, our results tell that security-centric language design can be effective in attaining strong security properties such as robust safety.
2023
2023 IEEE 36th Computer Security Foundations Symposium (CSF)
Piscataway, NJ USA
IEEE
979-8-3503-2192-0
Patrignani, M; Blackshear, S
Robust Safety for Move / Patrignani, M; Blackshear, S. - STAMPA. - (2023), pp. 308-323. (Intervento presentato al convegno csf tenutosi a Dubrovnik, Croatia nel 10-14 July 2023) [10.1109/CSF57540.2023.00045].
File in questo prodotto:
File Dimensione Formato  
rsmove.pdf

accesso aperto

Tipologia: Post-print referato (Refereed author’s manuscript)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 421.64 kB
Formato Adobe PDF
421.64 kB Adobe PDF Visualizza/Apri
Robust_Safety_for_Move.pdf

Solo gestori archivio

Tipologia: Versione editoriale (Publisher’s layout)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 474.7 kB
Formato Adobe PDF
474.7 kB Adobe PDF   Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/400876
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? 0
social impact