Long Term R&D: Security Proofs (proposal)

1. Summary

This is a motion proposal for the long-term R&D of the DFINITY Foundation, as part of the follow-up to this post: Motion Proposals on Long Term R&D Plans (Please read this post for context).

This project’s objective

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. In this project, the Foundation will first provide security proofs for the IC’s core components, and then prove that the IC securely glues these components together to provide precisely stated security guarantees.

2. Discussion lead

Gregory Neven

3. How this R&D proposal is different from previous types

Previous motion proposals have revolved around specific features and tended to have clear, finite goals that are delivered and completed. They tended to be measured in days, weeks, or months.

These motion proposals are different and are defining the long-term plan that the foundation will use, e.g., for hiring and organizational build-out. They have the following traits and patterns:

  1. Their scope is years, not weeks or months as in previous NNS motions
  2. They have a broad direction but are active areas of R&D so they do not have an obvious line of execution.
  3. They involve deep research in cryptography, networking, distributed systems, language, virtual machines, operating systems.
  4. They are meant to match the strengths of where the DFINITY foundation’s expertise is best suited.
  5. Work on these proposals will not start immediately.
  6. There will be many follow-up discussions and proposals on each topic when work is underway and smaller milestones and tasks get defined.

An example may be the R&D for “Scalability” where there will be a team investigating and improving the scalability of the IC at various stages. Different bottlenecks will surface and different goals will be met.

3. How this R&D proposal is similar to what we have seen

We want to double down on the behaviors we think have worked well. These include:

  1. Publicly identifying owners of subject areas to engage and discuss their thinking with the community
  2. Providing periodic updates to the community as things evolve, milestones reached, proposals are needed, etc…
  3. Presenting more and more R&D thinking early and openly.

This has worked well for the last 6 months so we want to repeat this pattern.

4. Next Steps

Developer forum intro posted
1-pager from the discussion lead posted
NNS Motion proposal submitted

5. What we are asking the community

  • Ask questions
  • Read 1-pager
  • Give feedback
  • Vote on the motion proposal

Frankly, we do not expect many nitty-gritty details because these are meant to address projects that go on for long time horizons.

The DFINITY foundation’s only goal is to improve the adoption of the IC so we want to sanity-check the projects we see necessary for growing the IC by having you (the ICP community) tell us what you all think of these active R&D threads we have.

6. What this means for the existing Roadmap or Projects

In terms of the current roadmap and proposals executed, those are still being worked on and have priority.

An intellectually honest way to look at this long-term R&D project is to see them as the upstream or “primordial soup” from which more baked projects emerge from. With this lens, these proposals are akin to asking, “what kind of specialties or strengths do we want to make sure DFINITY foundation has built up?”

Most (if not all) projects that the DFINITY foundation has executed or is executing are borne from long-running R&D threads. Even when community feedback tells the foundation, “we need X” or “Y does not work”, it is typically the team with the most relevant R&D area that picks up the short-term feature or project.

Please note:

Some folks gave asked if they should vote to “reject” any of the Long Term R&D projects as a way to signal prioritization. The answer is simple: “No, please, ACCEPT” :wink:

These long-term R&D projects are the DFINITY’s foundation’s thesis at R&D threads it should have across years (3 years is the number we sometimes use internally). We are asking the community to ACCEPT (pending 1-pager and more community feedback of course). Prioritization can come at a separate step.

Hi everyone!

My name is Gregory Neven, I’m a researcher in DFINITY’s security team.

We have quite a few researchers on our team who are pretty well-versed in provably secure protocol design, and our fingers are itching to get started on this project. I’m happy to answer any questions you may have!


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 that is at the basis of our Key Chain technology, threshold ECDSA that underlies Bitcoin integration on the IC, or our consensus protocol.

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 doesn’t 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 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 , @JensGroth

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

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

Proposal is live: Internet Computer Network Status