Towards Verifying the Bitcoin-S Library

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

[img]
Preview
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

Actions (login required)

View Item View Item
Provide Feedback