Document Open Access Logo

Towards Verifying the Bitcoin-S Library (Short Paper)

Authors Ramon Boss, Kai Brünnler, Anna Doukmak



PDF
Thumbnail PDF

File

OASIcs.FMBC.2020.8.pdf
  • Filesize: 399 kB
  • 9 pages

Document Identifiers

Author Details

Ramon Boss
  • Bern University of Applied Sciences, Switzerland
Kai Brünnler
  • Bern University of Applied Sciences, Switzerland
Anna Doukmak
  • Bern University of Applied Sciences, Switzerland

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

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)
    0
    PDF Downloads

References

  1. 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.
  2. 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.
  3. 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.
  4. Ramon Boss. Remove redundant function checkresult. Accessed 2019-07-03. URL: https://github.com/bitcoin-s/bitcoin-s/pull/565.
  5. 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.
  6. 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.
  7. LARA Lab, École Polytechnique Fédérale de Lausanne. Stainless documentation. Accessed 2019-06-19. URL: https://epfl-lara.github.io/stainless/.
  8. Oracle and/or its affiliates. Class BigInteger. Accessed 2019-07-03. URL: https://docs.oracle.com/javase/8/docs/api/java/math/BigInteger.html.
  9. 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.
  10. Suredbits & the bitcoin-s developers. The bitcoin-s website. Accessed 2019-06-19. URL: https://bitcoin-s.org.
  11. The bitcoin-s developers. The bitcoin-s repository. Accessed 2019-06-19. URL: https://github.com/bitcoin-s.
  12. The Stainless developers. Type aliases, type members, and dependent function types. Accessed 2019-06-27. URL: https://github.com/epfl-lara/stainless/pull/470.
  13. 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.
  14. Wikipedia contributors. Two’s complement. Accessed 2019-07-03. URL: https://en.wikipedia.org/wiki/Two%27s_complement.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail