Publication Types:

Verification of Bitcoin’s Smart Contracts in Agda using Weakest Preconditions for Access Control

blockchainconference
F. F. Alhabardi, A. Beckmann, B. Lazar, A. Setzer
27th International Conference on Types for Proofs and Programs (TYPES 2021)
Publication year: 2022

This paper addresses the verification of Bitcoin smart contracts using the interactive theorem prover Agda. It focuses on two standard smart contracts that govern the distribution of Bitcoins, Pay to Public Key Hash (P2PKH) and Pay to Multisig (P2MS). Both are written in Bitcoin’s low-level language script, and provide the security property of access control to the distribution of Bitcoins.

The paper introduces an operational semantics of the script commands used in P2PKH and P2MS, and formalises it in the Agda proof assistant using Hoare triples. It advocates weakest preconditions in the context of Hoare triples as the appropriate notion for verifying access control. Two methodologies for obtaining human-readable weakest preconditions are discussed in order to close the validation gap between user requirements and formal specification of smart contracts: (1) a step-by-step approach, which works backwards instruction by instruction through a script, sometimes stepping over several instructions in one go; (2) symbolic execution of the code and translation into a nested case distinction, which allows to read off weakest preconditions as the disjunction of accepting paths. A syntax for equational reasoning with Hoare Triples is defined in order to formalise those approaches in Agda.

Semantic Asset Administration Shells in Industry 4.0: A Survey

conferenceknowledge tech
S. Beden, Q. Cao, A. Beckmann
Proceedings of the 4th IEEE International Conference on Industrial Cyber-Physical Systems (ICPS), pp. 31-38
Publication year: 2021

The Asset Administration Shell (AAS) is a fundamental concept in the Reference Architecture Model for Industry 4.0 (RAMI 4.0), that provides a virtual and digital representation of all information and functions of a physical asset in a manufacturing environment. Recently, Semantic AASs have emerged that add knowledge representation formalisms to enhance the digital representation of physical assets. In this paper, we pro- vide a comprehensive survey of the scientific contributions to Semantic AASs that model the Information and Communication Layer within RAMI 4.0, and summarise and demonstrate their structure, communication, functionalities, and use cases. We also highlight the challenges of future development of Semantic AASs.

Modeling and Computing Available Rights for Algorithmic Licensing of Movies based on Blockchain

blockchainconference
Beckmann, A., Santos, J., Vijai Ananth, I.
The 5th International Conference on Future Networks & Distributed Systems (pp. 795-802). ACM.
Publication year: 2021

We consider the challenge of determining which rights are available for licensing within the context of algorithmic licensing of movies using blockchain technology. We model the space of rights using set theory. We define algorithms within our modelling context that implement basic transactions for our use case, and argue for their correctness. We evaluate our algorithms through experiments within a multi-node Hyperledger Fabric network, and establish the feasibility of our algorithms for the intended use case.

Total Search Problems in Bounded Arithmetic and Improved Witnessing

conference
Arnold Beckmann and Jean-Jose Razafindrakoto
24th International Workshop on Logic, Language, Information, and Computation (WoLLiC), 2017. Pages: 31 - 47
Publication year: 2017

We define a new class of total search problems as a subclass of Megiddo and Papadimitriou’s class of total $\NP$ search problems, in which solutions are verifiable in $\AC^0$. We denote this class $\forall\exists\AC^0$. We show that all total $\NP$ search problems are equivalent wrt. $\AC^0$-many-one reductions to search problems in $\forall\exists\AC^0$. Furthermore, we show that $\forall\exists\AC^0$ contains well-known problems such as the Stable Marriage and the Maximal Independent Set problems. We introduce the class of Inflationary Iteration problems in $\forall\exists\AC^0$ and show that it characterizes the provably total $\NP$ search problems of the bounded arithmetic theory corresponding to polynomial-time. Cook and Nguyen introduced a generic way of defining a bounded arithmetic theory $\VC$ for complexity classes $\C$ which can be obtained using a complete problem. For such $C$ we will define a new class $\KPT[C]$ of $\forall\exists\AC^0$ search problems based on Student-Teacher games in which the student has computing power limited to $\AC^0$. We prove that $\KPT[C]$ characterizes the provably total $\NP$ search problems of the bounded arithmetic theory corresponding to $\C$. All our characterizations are obtained via “new-style” witnessing theorems, where reductions are provable in a theory corresponding to $\AC^0$.

Hyper Natural Deduction

conference
Arnold Beckmann and Norbert Preining
Symposium on Logic in Computer Science (LICS), 2015, 30th Annual ACM/IEEE. Pages: 547 - 558
Publication year: 2015

We introduce a Hyper Natural Deduction system as an extension of Gentzen’s Natural Deduction system. A Hyper Natural Deduction consists of a finite set of derivations which may use, beside typical Natural Deduction rules, additional rules providing means for communication between derivations. We show that our Hyper Natural Deduction system is sound and complete for infinite-valued propositional Gödel Logic, by giving translations to and from Avron’s Hyper sequent Calculus. We also provide conversions for normalisation and prove the existence of normal forms for our Hyper Natural Deduction system.

Parity Games and Propositional Proofs

conference
Arnold Beckmann, Pavel Pudlák and Neil Thapen
38th International Symposium on Mathematical Foundations of Computer Science, MFCS 2013, Klosterneuburg, Austria, August 26-30, 2013. LNCS 8087. Pages: 111-122
Publication year: 2013

A propositional proof system is weakly automatizable if there is a polynomial time algorithm which separates satisfiable formulas from formulas which have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We also define a combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy.

Using Domain Specific Languages to Support Verification in the Railway Domain

conference
Phillip James, Arnold Beckmann, Markus Roggenbach
Hardware and Software: Verification and Testing. 8th International Haifa Verification Conference, HVC 2012 Haifa, Israel, November 6-8, 2012. Pages: 274 -275
Publication year: 2012

We explore the support of automatic verification via careful design of a domain specific language (DSL) in the context of algebraic specification. Formally a DSL is a loose specification the logical closure of which we regard as implicitly encoded “domain knowledge”. We systematically exploit this “domain knowledge” for automatic verification. We illustrate these ideas within the Railway Domain using the algebraic specification language Casl and an existing DSL, designed by Bjøerner, for modelling railways. Empirical evidence to the benefit of our approach is given in the form of the successful automatic verification of four railway track plans of real world complexity.

A Characterisation of Definable NP Search Problems in Peano Arithmetic

conference
Arnold Beckmann
Logic, Language, Information and Computation. 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Pages: 1 - 12
Publication year: 2009

The complexity class of $\prec$-bounded local search problems with goals is introduced for well-orderings $\prec$, and is used to give a characterisation of definable NP search problems in Peano Arithmetic.

On the computational complexity of cut-reduction

conference
Klaus T Aehlig and Arnold Beckmann
Logic in Computer Science, 2008. LICS '08. 23rd Annual IEEE Symposium on 24-27 June 2008. Pages: 284 - 293
Publication year: 2008

Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations, and explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.

On the complexity of parity games

conference
Arnold Beckmann and Faron G Moller
Visions of Computer Science — BCS International Academic Conference Imperial College, London, UK - 22 - 24 September 2008. Pages: 237 - 247
Publication year: 2008

Parity games underlie the model checking problem for the modal μ-calculus, the complexity of which remains unresolved after more than two decades of intensive research. The community is split into those who believe this problem – which is known to be both in NP and coNP – has a polynomial-time solution (without the assumption that P=NP) and those who believe that it does not. (A third, pessimistic, faction believes that the answer to this question will remain unknown in their lifetime.)

In this paper we explore the possibility of employing Bounded Arithmetic to resolve this question, motivated by the fact that problems which are both NP and coNP, and where the equivalence between their NP and coNP description can be formulated and proved within a certain fragment of Bounded Arithmetic, necessarily admit a polynomial-time solution. While the problem remains unresolved by this paper, we do proposed another approach, and at the very least provide a modest refinement to the complexity of parity games (and in turn the μ-calculus model checking problem): that they lie in the class of Polynomial Local Search problems. This result is based on a new proof of memoryless determinacy which can be formalised in Bounded Arithmetic.

The approach we propose may offer a route to a polynomial-time solution. Alternatively, there may be scope in devising a reduction between the problem and some other problem which is hard with respect to PLS, thus making the discovery of a polynomial-time solution unlikely according to current wisdom.

Propositional Logic for Circuit Classes

conference
Klaus T Aehlig and Arnold Beckmann
21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007. Pages: 512 - 526
Publication year: 2007

By introducing a parallel extension rule that is aware of independence of the introduced extension variables, a calculus for quantified propositional logic is obtained where heights of derivations correspond to heights of appropriate circuits. Adding an uninterpreted predicate on bit-strings (analog to an oracle in relativised complexity classes) this statement can be made precise in the sense that the height of the most shallow proof that a circuit can be evaluated is, up to an additive constant, the height of that circuit.

The main tool for showing lower bounds on proof heights is a variant of an iteration principle studied by Takeuti. This reformulation might be of independent interest, as it allows for polynomial size formulae in the relativised language that require proofs of exponential height.

Resolution Refutations and Propositional Proofs with Height-Restrictions

conference
Arnold Beckmann
In: Bradfield J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg, Pages 599 - 612.
Publication year: 2002

Height restricted resolution (proofs or refutations) is a natural restriction of resolution where the height of the corresponding proof tree is bounded. Height restricted resolution does not distinguish between tree- and sequence-like proofs. We show that polylogarithmic-height resolution is strongly connected to the bounded arithmetic theory S^1_2(\alpha) . We separate polylogarithmic-height resolution from quasi-polynomial size tree-like resolution. Inspired by this we will study infinitely many sub-linear-height restrictions given by functions n → 2_i((log^(i+1) n)^O(1)) for i ≥ 0 . We show that the resulting resolution systems are connected to certain bounded arithmetic theories, and that they form a strict hierarchy of resolution proof systems. To this end we will develop some proof theory for height restricted proofs.

A note on universal measures for weak implicit computational complexity

conference
Arnold Beckmann
9th International Conference, LPAR 2002, Tbilisi, Georgia, October 14-18, 2002, Pages: 53 - 67
Publication year: 2002

This note is a case study for finding universal measures for weak implicit complexity. We will instanciate “universal measures” by “dynamic ordinals”, and “weak implicit complexity” by “bounded arithmetic”. Concretely, we will describe the connection between dynamic ordinals and witness oracle Turing machines for bounded arithmetic theories.