OASIcs.FMBC.2020.8.pdf
- Filesize: 399 kB
- 9 pages
Document
Towards Verifying the Bitcoin-S Library (Short Paper)
Authors
-
Part of:
Volume:
2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-12-11
Cite AsGet BibTex
Ramon Boss, Kai Brünnler, and Anna Doukmak. Towards Verifying the Bitcoin-S Library (Short Paper). In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 8:1-8:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/OASIcs.FMBC.2020.8
https://doi.org/10.4230/OASIcs.FMBC.2020.8
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Logic and verification
Keywords
- Bitcoin
- Scala
- Bitcoin-S
- Stainless
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Régis Blanc and Viktor Kuncak. Sound reasoning about integral data types with a reusable SMT solver interface. In Philipp Haller and Heather Miller, editors, Proceedings of the 6th ACM SIGPLAN Symposium on Scala, Scala@PLDI 2015, Portland, OR, USA, June 15-17, 2015, pages 35-40. ACM, 2015. URL: https://doi.org/10.1145/2774975.2774980.
- Régis Blanc, Viktor Kuncak, Etienne Kneuss, and Philippe Suter. An overview of the leon verification system: verification by translation to recursive functions. In Proceedings of the 4th Workshop on Scala, SCALA@ECOOP 2013, Montpellier, France, July 2, 2013, pages 1:1-1:10. ACM, 2013. URL: https://doi.org/10.1145/2489837.2489838.
- Ramon Boss. Issue 519: Unknown type parameter type T in self referencing generic. Accessed 2019-06-27. URL: https://github.com/epfl-lara/stainless/issues/519.
- Ramon Boss. Remove redundant function checkresult. Accessed 2019-07-03. URL: https://github.com/bitcoin-s/bitcoin-s/pull/565.
- Ramon Boss. Transaction can reference two different outputs of the same previous transaction. Accessed 2019-06-19. URL: https://github.com/bitcoin-s/bitcoin-s/pull/435.
- Ramon Boss, Kai Brünnler, and Anna Doukmak. The bitcoin-s-verification repository. Accessed 2019-07-06. URL: https://github.com/kaibr/bitcoin-s-verification.
- LARA Lab, École Polytechnique Fédérale de Lausanne. Stainless documentation. Accessed 2019-06-19. URL: https://epfl-lara.github.io/stainless/.
- Oracle and/or its affiliates. Class BigInteger. Accessed 2019-07-03. URL: https://docs.oracle.com/javase/8/docs/api/java/math/BigInteger.html.
- Jimmy Song. Bitcoin Core Bug CVE-2018–17144: An Analysis. Accessed 2019-06-20. URL: https://hackernoon.com/bitcoin-core-bug-cve-2018-17144-an-analysis-f80d9d373362.
- Suredbits & the bitcoin-s developers. The bitcoin-s website. Accessed 2019-06-19. URL: https://bitcoin-s.org.
- The bitcoin-s developers. The bitcoin-s repository. Accessed 2019-06-19. URL: https://github.com/bitcoin-s.
- The Stainless developers. Type aliases, type members, and dependent function types. Accessed 2019-06-27. URL: https://github.com/epfl-lara/stainless/pull/470.
- Nicolas Voirol, Etienne Kneuss, and Viktor Kuncak. Counter-example complete verification for higher-order functions. In Philipp Haller and Heather Miller, editors, Proceedings of the 6th ACM SIGPLAN Symposium on Scala, Scala@PLDI 2015, Portland, OR, USA, June 15-17, 2015, pages 18-29. ACM, 2015. URL: https://doi.org/10.1145/2774975.2774978.
- Wikipedia contributors. Two’s complement. Accessed 2019-07-03. URL: https://en.wikipedia.org/wiki/Two%27s_complement.