Attack Tolerant Distributed Applications

Abstract:
Blockchain technology introduced in Bitcoin has been shown to be a solution to the Byzantine generals problem. Bitcoin and it's blockchain remain vulnerable to attack by various mechanisms such as DDOS (distributed denial of service) attacks, malware which can be disguised as official Bitcoin clients, or just bugs in the implementation of the Bitcoin specification. The blockchain in it's current implementations are not yet attack tolerent by design. This post includes some potential designs which borrow elements from the blockchain and from CRASH (Clean-slate Resilient Adaptive Secure Hosts) to produce attack tolerant distributed applications.

Introduction

In attack tolerant information systems correctness is essential. Correct by construction is an software engineering method where the code is formally specified, and the intended behavior of the code is formally verified as correct. Under this paradigm of thinking about software the program can be thought of as 'proofs' not unlike the paradigm of mathematics. The concept of 'program as proofs' can be considered a result of Curry-Howard correspondence also known as Curry–Howard isomorphism . Computational Trinitarianism builds upon these insights from Curry-Howard correspondence by forming a similar trinity now all that unlike the CIA triad in information security, where it's 1. propositions as types, 2. programs as proofs, 3. relations between type theory and category theory. This theory of computation breaks down into logic, language and categories.

Blockchain engineers are just beginning to move into the direction of verifiable computing, decidable computing, with the first example of this being Tauchain. Tauchain (Tau is short for tautology) is in development to be a secure decentralized high performance computing platform with unique properties. Tauchain is attempting to be the first true implementation of the semantic web, as it comes with it's own reasoner. Tauchain's design is novel in that in the Agoras context on the Tauchain there is to be a blockchain based consensus, but what makes this design unique is that Tauchain downloads and verifies itself, block by block, while Agoras creates a market around decentralized computation so that incentives are in place for people to rent out their computation to Tauchain. Tauchain is based on decideable logic, dependently typed programming, and utilizes authenticated data structures to allow for verifiable computation.

Evolvability is the key mechanism behind attack tolerance. In biological systems the immune system has evolved over time to thwart hostile invaders. In species, the species which are able to best adapt to change tend to survive the longest, and species which adapt the fastest are the most resilient. Resilience is a trait which we can see both in attack tolerant systems and in biological systems. Biomimicry is a method which can be used to import the solutions from biological systems into information systems and in this whitepaper there will be several information security solutions borrowed from biology.

Attack tolerant data structures

One mechanism of attack tolerant design is code variance. The security is through diversity of implementations of the specification, and through slight variations in the code such that the code runs as expected but is not exactly the same. These slight variations can be seen as mutations which can be adaptive so that the overall design can change on the fly.

A quote from the paper titled "Investigating correct by construction attack-tolerant systems" elucidates this:

Attack-tolerant distributed systems change their pro-tocols on-the-fly in response to apparent attacks from the envi-ronment; they substitute functionally equivalent versions possibly more resistant to detected threats. Alternative protocols can be packaged together as a single
adaptive protocol or variants from a formal protocol library can be sent to threatened groups of processes.

Variation serves a useful security purpose by providing a kind of diversity. An additional quote below describes

Using a constructive Logic of Events based on Compu-
tational Type Theory (CTT) [ABC06], [CB08], [Bic09] we
have been able to formally specify safety and liveness prop-
erties for distributed protocols and synthesize executable code
from constructive proofs that the specifications are realizable
[CB08]. We have used this proofs-as-processes method to build fault-tolerant protocols, provably secure protocols, and
adaptive protocols [LKvR+99]

Adaptive protocols

In order to have the basis for an attack tolerant information system you must have correctness which means a correct-by-construction approach which you also combine with adaptive protocols. So you need both provably secure protocols with adaptiveness so that if a particular version of the protocol is attacked it can in a way mutate to negate or nullify the attack if the attack is against a specific implementation of a component for example. There may be multiple proofs to solve a particular challenge or problem in a protocol, and the ability of the software to switch between formal proofs is what can help the software to adapt on the fly.

Theoretically a software platform can contain a library of proofs. These proofs could exist in a knowledge base, or in a way where a particulate proof can be activated to replace the current version of the proof in executable form. So for example you may have three ways to solve a problem, a, b, and c, and depending on the circumstances any of these could be activated. It is the equivalent to having plan a, plan b, plan c, in formal proofs with guaranteed correctness, but also the ability to swap out or replace the current plan if an attack is detected and occurring.

In a blockchain data structure you might be able to change certain parameters to adapt to an attack. The ability to dial up decentralization or dial down, the ability to raise costs of transactions or lower, but at the same time at the level of proofs a blockchain itself is just a data structure which could be swapped out for an equivalent data structure if the circumstances require it. This would mean security and adaptiveness is the priority rather than attachment to a particular proof which is only intended to solve a problem.

The proof database

As we know, programs are proofs. If we know programs are proofs and we have the ability to reuse proofs then having a library or database of proofs is a key component to this kind of adaptabilty. In addition if we want the human touch then we can let human beings curate and participate in the selection process. The blockchain data structure would be reduced to a formal proof, as would the directed acyclic graph, as would algorithms like page-rank, all exist to solve some particular problem, all could be added to a database of proofs, all proofs in the database could be reviewed, curated by humans, until a best practices or best fit for purpose is discovered for various proofs.

We may learn blockchains aren't the best data structure for promotion of security in every context. We may discover the top data structures for sol.ving a particular problem and it may be a searchable database. In the near future it is possible that programmers will search for proofs to solve their problem from a database and over time it might even be possible for this to become automated.

The artificial immune system

The artificial immune system is what allows for self-healing, recovery, immunity, and when you have an adaptive system this immunity allows the system to adapt in a favorable way to maintain homeostasis. Attacks would be detected, the library of useful proofs would be gradually expanded, small variations on the proofs would be applied for synthetic diversity while the proofs would function the exact same, and threats could be isolated or quarantined. Swarm intelligence can greatly benefit an artificial immune system, and the human touch of curation can help also.

Human beings contribute human computation and can generate proofs. In fact, the human and machine intelligence work together to solve some of the most difficult problems. The mathematician may use a computer to act as an automated theorem prover. A musician may program a computer to create generative art which adapts to the audience. This ability for humans to contribute would allow an artificial immune system to benefit from human creativity and humans may be able to see certain attacks before any artificial intelligence. The question is how to integrate human decision making into an artificial immune system.

Future considerations

Future considerations include fully homomorphic encryption, privacy enhanced partially homomorphic encryption, swarm intelligence, distributed artificial neuro-networks, and more.

References

Constable, R., Bickford, M., & Van Renesse, R. (2011). Investigating correct-by-construction attack-tolerant systems.

Mazurczyk, W., Drobniak, S., & Moore, S. (2015). Towards a Systematic View on Cybersecurity Ecology. arXiv preprint arXiv:1505.04207.

Miller, A., Hicks, M., Katz, J., & Shi, E. Authenticated Data Structures, Generically.

Miller, A., & LaViola Jr, J. J. (2014). Anonymous byzantine consensus from moderately-hard puzzles: A model for bitcoin. Retrieved from Anonymous Byzantine Consensus from Moderately-Hard Puzzles: A Model for Bitcoin.

Van Renesse, R., Bickford, M., & Constable, R. (2011). Investigating correct-by-construction attack-tolerant systems.