License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2020.8
URN: urn:nbn:de:0030-drops-134212
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13421/
Boss, Ramon ;
Brünnler, Kai ;
Doukmak, Anna
Towards Verifying the Bitcoin-S Library (Short Paper)
Abstract
We try to verify properties of the Bitcoin-S library, a Scala implementation of parts of the Bitcoin protocol. We use the Stainless verifier which supports programs in a fragment of Scala called Pure Scala. Since Bitcoin-S is not written in this fragment, we extract the relevant code from it and rewrite it until we arrive at code that we successfully verify. In that process we find and fix two bugs in Bitcoin-S.
BibTeX - Entry
@InProceedings{boss_et_al:OASIcs:2020:13421,
author = {Ramon Boss and Kai Br{\"u}nnler and Anna Doukmak},
title = {{Towards Verifying the Bitcoin-S Library (Short Paper)}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {8:1--8:9},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bruno Bernardo and Diego Marmsoler},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13421},
URN = {urn:nbn:de:0030-drops-134212},
doi = {10.4230/OASIcs.FMBC.2020.8},
annote = {Keywords: Bitcoin, Scala, Bitcoin-S, Stainless}
}
|
Keywords: |
|
Bitcoin, Scala, Bitcoin-S, Stainless |
|
Collection: |
|
2nd Workshop on Formal Methods for Blockchains (FMBC 2020) |
|
Issue Date: |
|
2020 |
|
Date of publication: |
|
11.12.2020 |
|
Supplementary Material: |
|
The original Bitcoin-S code we started from, the extracted code, and the finally verified code are available in our GitHub repository: https://github.com/kaibr/bitcoin-s-verification. |
