Research Project: Lex Leibniz
Smart contracts on cryptocurrency platforms carry large amounts of monetary value, but have been prone
to flaws and security vulnerabilities that have resulted in large financial losses.
This project is investigating the development of a high level smart contract language, suitable for the representation
of financial contracts, that better supports the development of correct and secure smart contracts.
We are investigating the fundamental principles of smart contract verification, and developing ways of expressing
financial contracts as smart contracts in ways that are more easily comprehensible to their users,
and supports verification of both correctness and security.
The core methodological principle underlying the work is the use
of declarative representations of smart contracts and their
specifications. We will draw on earlier contributions to logic
programming, deontic logic (the logic of permission, obligation
and prohibition), work on logics for authentication and
authorization in cryptographic settings and linear logic (as a
representation of resource production, preservation and
consumption).
Staff:
Prof. Ron van der Meyden (CSE), Prof. Michael Maher (ADFA and Reasoning Research Institute),
Outcomes:
- On the specification and verification of atomic swap smart contracts (extended abstract), Proc. IEEE International Conference on Blockchain and Cryptocurrency 2019, R. van der Meyden.
(Full version: arXiv:1811.06099, Nov 2018)
- A Formal Treatment of Contract Signature, Ron van der Meyden, to appear, IEEE Transactions on Services Computing. DOI:10.1109/TSC.2021.3101833 (Accepted version on Arxiv:
arXiv:2002.09827).
Related earlier work:
- [J11] A logical reconstruction of SPKI,
J.Y. Halpern and R. van der Meyden,
Journal of Computer Security, Volume 11, Issue 4, 2003,. pp 581-614.
(a special issue of Journal of Computer Security containing selected papers from CSFW'01.)
- [J7]
A logic for SDSI's Linked Local Name Spaces , J. Y. Halpern and
R. van der Meyden, Journal of Computer Security, vol. 9, number
1,2, pp. 75 - 104, 2001. (a special issue of the Journal of
Computer Security containing selected papers from CSFW 99.)
- [J3] The Dynamic Logic of
Permission, R. van der Meyden, Journal of Logic and
Computation, Vol 6, No. 3 pp. 465-479, 1996. A version of this
paper appeared at the IEEE Symposium on Logic in Computer
Science, Philadelphia, 1990.
- [C4]
A Clausal Logic for Deontic Action Specification, R. van der Meyden,
Proceedings of the International Logic Programming Symposium,
San Diego, October 1991, pp. 221-238. MIT Press.