Formal Model Guided Conformance Testing for Blockchains
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929681543987200 |
|---|---|
| author | Drobnjakovic, Filip Kashapov, Amir Kupresanin, Matija Scholz, Bernhard Subotic, Pavle |
| author_facet | Drobnjakovic, Filip Kashapov, Amir Kupresanin, Matija Scholz, Bernhard Subotic, Pavle |
| contents | Modern blockchains increasingly consist of multiple clients that implement a single blockchain protocol. If there is a semantic mismatch between the protocol implementations, the blockchain can permanently split and introduce new attack vectors. Current ad-hoc test suites for client implementations are not sufficient to ensure a high degree of protocol conformance. As an alternative, we present a framework that performs protocol conformance testing using a formal model of the protocol and an implementation running inside a deterministic blockchain simulator. Our framework consists of two complementary workflows that use the components as trace generators and checkers. Our insight is that both workflows are needed to detect all types of violations. We have applied and demonstrated the utility of our framework on an industrial strength consensus protocol. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_08550 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Formal Model Guided Conformance Testing for Blockchains Drobnjakovic, Filip Kashapov, Amir Kupresanin, Matija Scholz, Bernhard Subotic, Pavle Cryptography and Security Logic in Computer Science Software Engineering Modern blockchains increasingly consist of multiple clients that implement a single blockchain protocol. If there is a semantic mismatch between the protocol implementations, the blockchain can permanently split and introduce new attack vectors. Current ad-hoc test suites for client implementations are not sufficient to ensure a high degree of protocol conformance. As an alternative, we present a framework that performs protocol conformance testing using a formal model of the protocol and an implementation running inside a deterministic blockchain simulator. Our framework consists of two complementary workflows that use the components as trace generators and checkers. Our insight is that both workflows are needed to detect all types of violations. We have applied and demonstrated the utility of our framework on an industrial strength consensus protocol. |
| title | Formal Model Guided Conformance Testing for Blockchains |
| topic | Cryptography and Security Logic in Computer Science Software Engineering |
| url | https://arxiv.org/abs/2501.08550 |