Distributed computing has by now become a pervasive technology due to the widespread adoption of electronic devices connected by the Internet infrastructure, which are used by individuals, companies, and institutions to perform an increasing number of daily activities in a digital mode. One of the most prominent examples over the last decade is blockchain technology. It results in a distributed ledger that permanently records transactions taking place among untrusted parties in a decentralized and disintermediated environment, which was devised after the global financial crisis of 2008 to avoid the double spending problem in virtual currency platforms.
A blockchain is an append-only ledger that collects transactions. It is composed of blocks linked together through cryptography, each one containing the hash value of the previous block, a timestamp, and transaction data. Once stored, a data block cannot be altered or removed from the blockchain without compromising the validity of all the subsequent blocks. This immutability property certifies that transaction data residing in the blockchain are tamper-proof, thus guaranteeing that everyone can trust the blockchain. The parties form a peer-to-peer communication network adhering to a consensus protocol for block validation. Usually a blockchain is public, meaning that the ledger is accessible by anyone without specific read, write, or validate permissions, with the users being free to enter, leave, and join again the network at any time. Transaction validation is accomplished algorithmically, with no central authority, through a computationally expensive mechanism that discourages potential attackers.
A number of shortcomings affect public, permissionless blockchains, such as the excessive energy consumption required by the consensus protocol and conflicts between data immutability and regulations (right to be forgotten and transaction invalidation due to digital identity theft or contract nullity or infringement, just to mention a few). In the specific case of innovative payment methods, there are also risks of losing monetary sovereignty and undermining financial stability, as witnessed by the fact that many central banks are exploring the issuance of what is called central bank digital currency (CBDC), which would also reduce the costs associated with managing physical cash, promote financial inclusion, and hopefully discourage tax evasion, money laundering, and other illegal activities. As a consequence private, permissioned blockchains are getting momentum, as they could ultimately give businesses a greater degree of control. The reason is that they can be accessed only by authorized people and are governed by a designated person, enterprise, or authority. Methods for reversing illegal transactions are thus needed in a private blockchain, as well as unauthorized information flows from its governance to the various parties must be avoided.
Developing complex distributed systems like private blockchains is extremely challenging in terms of guaranteeing high levels of proper functioning, data protection, and quality of service. It even becomes a critical issue in CBDC platforms, where errors, data breaches, and poor performance may have economical and social consequences hard to estimate. This calls for a model-based approach in the early design stages so as to enable system property prediction.
The NiRvAna project is about the use of formal methods for the compositional modeling of functional and non-functional aspects of the behavior and the structure of private blockchains. On the analysis side, the focus will be on relevant properties such as noninterference and reversibility. The former is concerned with the absence of information leakage, due to qualitative or quantitative covert channels, from the private blockchain governance to permissioned users. The latter deals with undoing transactions, because of regulation compliance, in a way that timely brings the system back to a previous consistent state. This will be accomplished by developing or extending modeling languages, analysis techniques, and software tools according to a holistic view of trustworthiness that encompasses safety, security, integrity, efficiency, availability, resilience, and ease of use.
Freely inspired by w3.css