Internet Computer Association

DFINITY Foundation

Build long term R&D efforts for Security Proofs (from which multiple projects will emerge)



# Motion Proposal for Security Proofs

## 1. Objective

Prove the security of core cryptographic components of the IC, and create a security model and proof showing how the IC combines these components to provide well-defined security guarantees.

## 2. Background

The Internet Computer is a complex beast that requires several non-standard cryptographic primitives to come together in order to provide its strong security guarantees. Provable security, also known as reductionist security, is a technique from theoretical cryptography where a new scheme, protocol, or system is mathematically proved to be secure as long as some precisely stated hardness assumptions hold. The Foundation already used this technique to validate some of our core cryptographic components, such as the [non-interactive distributed key generation](https://eprint.iacr.org/2021/339) that is at the basis of our Key Chain technology, [threshold ECDSA](https://eprint.iacr.org/2021/1330) that underlies Bitcoin integration on the IC, or our [consensus protocol](https://eprint.iacr.org/2021/632).

## 3. Why this is important

Provable security is the main scientific design technique in modern cryptography and has become a requirement in the selection of many practical schemes and standards. Published security proofs will enable the community to analyze the protocol in all its details and verify its security. At the same time, they also allow us to make extra sure that the protocol does not have any hidden flaws.

## 4. Topics under this project

In a first phase, the Foundation will extend this approach to a number of other core components, e.g., the tree hash scheme that is used to hash the replicated state, the streaming signature scheme that secures cross-subnet communication, our gossip protocol, or the Internet Identity system.

In a second phase, the Foundation will validate the way these pieces are glued together to build more complex features (e.g., state synchronization, multi-subnet execution, disaster recovery) and, in the end, the full Internet Computer.

Correctly modeling security is a big part of the challenge here. One has to design models that cover the different aspects of security (integrity/safety, availability/liveness, as well as confidentiality/privacy) and that are simple enough for humans to get their heads wrapped around writing and verifying security proofs, yet are expressive enough to provide meaningful security guarantees in the real world. Because there are so many subcomponents and moving parts to the IC, most likely using a composable proof framework, e.g., the Universal Composability framework, to manage the complexity.

During both phases, this activity will keep a close link with the [Formal Verification](https://forum.dfinity.org/t/long-term-r-d-formal-verification-proposal/9397) effort that investigates the use of automated tools such as model checkers and theorem provers to provide strong security guarantees. One can expect strong synergies to come up between both approaches, especially in those components where manual proofs become too complex for human beings.

## 5. Key milestones (and technical solution if known)

* Published security proofs of selected components, possibly including
  * tree hash algorithm
  * streaming signatures
  * Internet Identity
* Selection of provable security frameworks to model security of the IC and modularize its security proof
* Security model and proof of the Internet Computer

## 6. Discussion leads

Gregory Neven, Jens Groth

# 7. Why the DFINITY Foundation should make this a long-running R&D project

Creating security models and proofs is a time-consuming activity, even for small cryptographic components. A security proof for the complete Internet Computer is a very ambitious endeavor that would rank it among the most complex systems that have ever been analyzed using this technique. Automated security proofs will be used wherever possible, but reconciling (manual) computational proofs and (automatable) formal methods is still a nascent field of research.

# 8. Skills and Expertise necessary to accomplish this (maybe teams?)

Cryptographic protocol design and analysis

Provable security frameworks and techniques

Formal methods

Teams involved: Research team (formal security), Crypto, Consensus, Message Routing, Networking, Execution, Crypto Layer 2 - II

# 9. Open Research questions

* Are the core cryptographic components of the IC provably secure?
* What type of security guarantees can the IC provably provide (integrity, liveness, fairness,...) and under what assumptions?
* Are these guarantees just worst-case lower bounds, or can they also be used to estimate efficiency and security of the IC in more optimistic real-life scenarios?
* Which technique is better suited to analyze the security of a large cryptographic system like the IC, manual reductionist proof or automated formal methods? Can they be combined in a meaningful way?

# 10. Examples where community can integrate into project

Provide input as to which components the community considers most crucial to analyze first, and which aspects of security the community cares most about.

Peer reviewing of the security proofs before and after publication

# 11. What we are asking the community

* Review comments, ask questions, give feedback
* Vote accept or reject on NNS Motion
* Participate in technical discussions as the motion moves forward



Developer forum: https://forum.dfinity.org/t/long-term-r-d-security-proofs-proposal/9398/3





Long Term R&D: Security Proofs