Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2512.04755 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917435765948416 |
|---|---|
| author | Lybech, Stian Gorla, Daniele Aceto, Luca |
| author_facet | Lybech, Stian Gorla, Daniele Aceto, Luca |
| contents | This paper develops semantic typing in a smart-contract setting to ensure type safety of code that uses statically untypable language constructs, such as the fallback function. The idea is that the creator of a contract on the blockchain equips code containing such constructs with a formal proof of its type safety, given in terms of the semantics of types. Then, a user of the contract only needs to check the validity of the provided 'proof certificate' of type safety. This is a form of proof-carrying code, which naturally fits with the immutable nature of the blockchain environment. As a concrete application of our approach, we focus on ensuring information flow control and non-interference for TinySol, a distilled version of the Solidity language, through security types. We provide the semantics of types in terms of a typed operational semantics of TinySol and we express the proofs of safety as coinductively-defined typing interpretations, which can be represented compactly via up-to techniques, similar to those used for bisimilarity. We also show how our machinery can be used to type the typical pointer-to-implementation pattern based on the fallback function and to reject a distilled version of the infamous Parity Multisig Wallet Attack. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_04755 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts Lybech, Stian Gorla, Daniele Aceto, Luca Programming Languages This paper develops semantic typing in a smart-contract setting to ensure type safety of code that uses statically untypable language constructs, such as the fallback function. The idea is that the creator of a contract on the blockchain equips code containing such constructs with a formal proof of its type safety, given in terms of the semantics of types. Then, a user of the contract only needs to check the validity of the provided 'proof certificate' of type safety. This is a form of proof-carrying code, which naturally fits with the immutable nature of the blockchain environment. As a concrete application of our approach, we focus on ensuring information flow control and non-interference for TinySol, a distilled version of the Solidity language, through security types. We provide the semantics of types in terms of a typed operational semantics of TinySol and we express the proofs of safety as coinductively-defined typing interpretations, which can be represented compactly via up-to techniques, similar to those used for bisimilarity. We also show how our machinery can be used to type the typical pointer-to-implementation pattern based on the fallback function and to reject a distilled version of the infamous Parity Multisig Wallet Attack. |
| title | Typing Fallback Functions: A Semantic Approach to Type Safe Smart Contracts |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2512.04755 |