Boss, Ramon; Brünnler, Kai; Doukmak, Anna (11 December 2020). Towards Verifying the Bitcoin-S Library In: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany 10.4230/OASIcs.FMBC.2020.8
|
Text
OASIcs-FMBC-2020-8.pdf Available under License Creative Commons: Attribution (CC-BY). Download (408kB) | Preview |
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.
Item Type: |
Conference or Workshop Item (Paper) |
---|---|
Division/Institute: |
School of Engineering and Computer Science > Research Institute for the Security in the Information Society RISIS School of Engineering and Computer Science > Institute for Cybersecurity & Engineering (ICE) |
Name: |
Boss, Ramon; Brünnler, Kai and Doukmak, Anna |
Subjects: |
Q Science > QA Mathematics Q Science > QA Mathematics > QA75 Electronic computers. Computer science Q Science > QA Mathematics > QA76 Computer software |
Publisher: |
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany |
Language: |
English |
Submitter: |
Kai Brünnler |
Date Deposited: |
25 Jan 2021 14:59 |
Last Modified: |
25 Jan 2021 14:59 |
Publisher DOI: |
10.4230/OASIcs.FMBC.2020.8 |
ARBOR DOI: |
10.24451/arbor.14259 |
URI: |
https://arbor.bfh.ch/id/eprint/14259 |