Network Working Group C. A. Wood Internet-Draft Cloudflare Intended status: Informational 13 March 2023 Expires: 14 September 2023 Challenges, Opportunities, and Directions for Formal Analysis in the IETF and IRTF draft-analysis-challenges-00 Abstract This document discusses challenges, opportunities, and directions for formal analysis of protocols developed in the IETF. About This Document This note is to be removed before publishing as an RFC. Status information for this document may be found at https://datatracker.ietf.org/doc/draft-analysis-challenges/. Source for this draft and an issue tracker can be found at https://github.com/chris-wood/draft-analysis-challenges. Status of This Memo This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79. Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet- Drafts is at https://datatracker.ietf.org/drafts/current/. Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress." This Internet-Draft will expire on 14 September 2023. Copyright Notice Copyright (c) 2023 IETF Trust and the persons identified as the document authors. All rights reserved. Wood Expires 14 September 2023 [Page 1] Internet-Draft Formal Analysis Challenges March 2023 This document is subject to BCP 78 and the IETF Trust's Legal Provisions Relating to IETF Documents (https://trustee.ietf.org/ license-info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document. Table of Contents 1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 2 2. Conventions and Definitions . . . . . . . . . . . . . . . . . 4 3. Analysis Overview . . . . . . . . . . . . . . . . . . . . . . 4 4. Analysis Challenges and Open Problems . . . . . . . . . . . . 5 4.1. Timelines . . . . . . . . . . . . . . . . . . . . . . . . 5 4.2. Tooling . . . . . . . . . . . . . . . . . . . . . . . . . 6 4.3. Incentives . . . . . . . . . . . . . . . . . . . . . . . 7 4.4. Complexity and Precision . . . . . . . . . . . . . . . . 7 4.5. Resource Limits . . . . . . . . . . . . . . . . . . . . . 8 5. Security Considerations . . . . . . . . . . . . . . . . . . . 9 6. IANA Considerations . . . . . . . . . . . . . . . . . . . . . 9 7. References . . . . . . . . . . . . . . . . . . . . . . . . . 9 7.1. Normative References . . . . . . . . . . . . . . . . . . 9 7.2. Informative References . . . . . . . . . . . . . . . . . 10 Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . 11 Author's Address . . . . . . . . . . . . . . . . . . . . . . . . 11 1. Introduction The IETF and IRTF produce technical specifications for protocols used on the Internet. Applications use these technical specifications in shipping software. Often times, use of these technical specifications has a direct impact on end users of the Internet. As an obvious example, TLS 1.3 [TLS13] is the de-facto transport security protocol used on the Internet, protecting data in transit between different different parties on the Internet. The process by which TLS 1.3 was developed was unique for its time. In the wake of one too many security problems with prior versions of the protocol, TLS 1.3 was developed in close collaboration with security researchers to ensure that the resulting design and specification provided provably secure properties that one would expect from such a protocol. The process took years and resulted in dozens of academic publications and interoperable implementations, further improving the community's confidence in the result. And in the end, the work paid off: TLS 1.3 has be safely deployed at scale for years without any significant issues. Wood Expires 14 September 2023 [Page 2] Internet-Draft Formal Analysis Challenges March 2023 Several IETF protocols since TLS 1.3 have built on the process by which it was developed, including QUIC [RFC9000], MLS [MLS], Oblivious HTTP [OHTTP], and Privacy Pass [PRIVACYPASS]. Each of these published and developing specifications have incorporated security analysis into the process by which the specifications are ratified. Formal analysis gives us confidence in the protocols we specify and deploy. It advocates for a rigorous approach to defining protocols and describing their security properties. Failure to apply formal analysis does not definitively yield protocols with known flaws, but it can lead to security failures in practice. Infamous examples as of late include Matrix, Telegram, PGP, and various configurations of TLS 1.2 and earlier versions. In contrast, applying formal analysis helps demonstrate that certain classes of attacks are not applicable. While this does not necessarily rule out attacks entirely, since modeling and analysis is always imprecise and requires simplifying compromise, it has the potential to more consistently yield better outcomes. However, there are still plenty of examples of technical specifications that lack any sort of formal analysis. Lack of formal analysis is problematic for a number of reasons, including, though not limited to, the following: 1. Real world vulnerabilities. Protocol specifiations may be developed with security or privacy vulnerabilities. Such vulnerabilities can lead to real problems for end users. In this sense, publishing specifications without formal analysis is akin to testing software in production, yet is uniquely worse since updating specifications requires IETF processes to enact and takes time. 2. Specification misuse. Formal analysis requires a certain degree of precision and rigor in which specifications for algorithms, protocols, and systems are described. This precision helps refine the interface for these types of objects. Lack of analysis can therefore lead to misuse of the object. This can in turn lead to undesired outcomes, including even security vulnerabilities. 3. Audience confusion. Protocol specifications without analysis may lack precision or specificity that often comes from formal analysis, yielding complex documents that are difficult to understand, use, and deploy in practice. Wood Expires 14 September 2023 [Page 3] Internet-Draft Formal Analysis Challenges March 2023 Lack of formal analysis comes from a variety of reasons. This document summarizes some of those problems and discusses opportunities for potential solutions and new directions the community can explore to improve the situation. It is meant to encourage discussion, not be published as an RFC. 2. Conventions and Definitions The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals, as shown here. 3. Analysis Overview As the IETF is primarily tasked with producing technical specifications for protocols, analysis of these protocols can benefit greatly from computer-aided tools. For example, [ProVerif] and [Tamarin] are both tools that protocol designers can use to model their protocol, attacker, and prove (or disprove) certain properties of the protocol. As with any modeling tool, these are limited both by the specificity of the model as well as the questions that are asked of the model. For example, security protocol models often make simplifying assumptions about the underlying cryptographic objects used in the protocol, whereas in practice these objects may break over time. Hand-written proofs complement computer-aided, machine- checked proofs. These proofs are often more complicated since they more accurately model all aspects of the protocol. As a result, these proofs yield mathematically precise statements of security. Regardless of the mechanism, analysis generally follows the following recipe: 1. Specify the threat model, including the attacker and its capabilities. 2. Specify the security goals with respect to this threat model. 3. Describe whether the security goals are met and, if and when they are not met, a description of how they are not met through an exemplary attack that violates the goal. Applicable attacks are often accompanied with explanations of why they are out of scope or how applications and deployments can deal with the attack in practice. Wood Expires 14 September 2023 [Page 4] Internet-Draft Formal Analysis Challenges March 2023 The order of these tasks is not always the same, but the content is generally consistently applied. What differs across technical specifications is the rigor through which these tasks are achieved. As an example, TLS 1.3 (Appendix E of [TLS13]) includes a list of security properties and, for each property, describes the attacker model in which these properties are satisfied. It additionally points to relevant, peer reviewed formal analysis work that demonstrates validity of these claims. QUIC [QUIC] lists various types of attacker models and, within each attacker model, the types of attacks that are possible. However, unlike [TLS13], does not have backing formal analysis for all of claims about attack resistance. As another example, Oblivious HTTP [OHTTP] takes an even different approach by informally describing the threat model and security goals of the protocol, with a reference to backing analysis (that did not receive peer review) with Tamarin. 4. Analysis Challenges and Open Problems This section describes some high level problems that impact the scale at which the IETF and IRTF applies formal analysis to technical specifications. 4.1. Timelines Sometimes formal analysis does not occur due to mismatched timelines. Formal analysis takes time, and that time may not align with the desired pace at which a technical specification moves towards publication. The general requirement for advancing technical specifications in IETF and IRTF groups is rough consensus and running code, and those are often easier to achieve than formal analysis. In many cases, the pressure to ship or otherwise advance specifications often trumps the desire for formal analysis. Analysis is time consuming, perhaps even more so than the development of the specification itself. While the iterative process TLS 1.3 established between specification, analysis, and experimentation is ideal, often times many protocols are fully specified prior to analysis. Applying analysis after specification in sequence, rather than in applying analysis in parallel with protocol specification, means that the result on publishing time is worsened. Overcoming this challenge may require a change in the way in which we establish consensus for technical specifications. Some possibilities are below. 1. Establish a set of common questions and formal process for formal analysis. This may include, for example, a template by which analysis findings may be documented, as well as key questions to Wood Expires 14 September 2023 [Page 5] Internet-Draft Formal Analysis Challenges March 2023 ask. It may also include standardized notation that document editors can use for noting analysis-relevant questions and issues in their protocol documents. 2. Seek out formal analysis for working group documents as soon as possible after adoption. This helps ensure that analysis occurs in line with protocol specification to the maximum extent possible. 3. Encourage protocol editors and expert reviewers to share analysis results with the relevant working group(s) as early as possible. If possible, these findings can be shared during in-person meetings, but may also be shared on the mailing list. 4.2. Tooling Another barrier to scaling formal analysis is the state of tooling. While there exists a wide variety of tools by which protocol designers can model and analyze their protocol, including [ProVerif] and [Tamarin], not all tools are easy-to-use for protocol designers or provide the necessary set of features required for analysis. For example, modeling privacy -- for some definition of privacy -- is often a difficult task with tools like Tamarin and ProVerif. There may be multiple ways by which these obstacles are overcome. For example, the community might invest or otherwise contribute to the ongoing development and maintenance of these tools. In general, they are often maintained by academic researchers, including graduate students, who leave the project or move on to other things over time. Like an critical open source project, these tools require consistent and reliable support to encourage continued maintenance and development to better fit the needs of the community. Beyond explicit tooling support, the amount of educational resources available for consumption, including examples, demos, running code, etc., could be improved and made more approachable for newcomers. While there exists plenty of learning material for these tools, they are often oriented towards those with a background or familiarity with formal methods. Educational material oriented towards engineers is needed. Wood Expires 14 September 2023 [Page 6] Internet-Draft Formal Analysis Challenges March 2023 4.3. Incentives Lack of incentives is a large barrier to adopting formal analysis in practice. From a research perspective, there is often little incentive to work on formal analysis for "uninteresting" or "overly simple" protocols, including those that seem to be "obviously correct." Publishing formal analysis with negative results, i.e., which demonstrate that there are no problems with a technical specification, is often challenging. And without proper publishing incentives, there is little incentive for academic researchers to spend time on this type of work. Addressing this problem may require establishing a venue for more easily publishing formal analysis without compromising on the quality of peer review. Such venue should make clear that publishing analysis of any type is appropriate, including formal models, pen and paper proofs, and so on. From the specification editor's perspective, sometimes analysis can seem unnecessary, perhaps because the object being specified is indeed "obviously correct" or that security considerations with proven interoperability seem sufficient. However, as has been demonstrated, security considerations are not a suitable replacement for security analysis. In general, the problem here seems to be that the type of analysis that would be sufficient to provide confidence in the specification is not clear. The IETF and IRTF community needs guidance on what type of analysis is appropriate. As obvious examples, cryptographic algorithms require analysis. Network protocols such as TLS also require analysis, but of a different type. The community could work on collecting examples of formal analyses to use as guidance in determining the suitable amount of analysis. 4.4. Complexity and Precision Specification complexity is a barrier to analysis. Complexity makes it challenging to develop an accurate mental model for the problem being solved, which is necessary for defining and refining the threat model and desired security properties of a protocol. Complexity makes the learning curve steep, deterring otherwise willing contributors from working on the analysis. Complexity can be dealt with by breaking down specifications into smaller, purpose-specific pieces, where possible. Beyond helping tame complexity, this might also help enable better reuse of existing analysis results. Complexity might also be dealt with by improving the presentation quality of specifications, e.g., by using consistent vocabulary across related specifications, including more discusson about intuition, and so on. Wood Expires 14 September 2023 [Page 7] Internet-Draft Formal Analysis Challenges March 2023 Specifications also sometimes suffer from lack of precision. Naturally, as specifications are written in English, they are prone to misinterpretations by different people, especially those for whom English is not a native language. While prose is useful for describing intution, it is often insufficient for rigorous technical details. Lack of precision therefore makes analysis difficult since there lacks clarity on what is the exact object or syntax being specified. Use of more rigorous specification language, e.g., consistently presented and readable pseudocode, formal grammars, state machine descriptions, etc can all help improve the precision by which specifications are represented. However, it's worth noting that sometimes precision can increase specification complexity. Balancing these two is not always easy in practice. 4.5. Resource Limits Analysis is also impeded by a limitation of resources. Formal analysis is not an easy task. The tools, techniques, and methodologies for applying formal analysis vary in maturity, and the people generally capable of contributing such analyses are far fewer than the number required to analyze all known protocols. Moreover, the domain expertise required to formulate and represent and describe a suitable threat model is often difficult to acquire for those that do have the skills to perform formal analysis. For better or worse, specification editors are often not equipped to formulate problem statements, threat models, and security definitions. Specification editors can take steps to help bridge the gap between themselves and those capable of performing protocol design and analysis. Some possible actions are below. 1. Identify and collaborate with domain experts who might offer expertise for their protocol. If domain experts are unknown, consult the WG chairs or security area contributors for assitance. 2. Include the protocol's desired security properties and threat model in the protocol document. This can be done in the security considerations or elsewhere, but including it somewhere helps give domain experts and reviewers a target for analysis. 3. Include known implementations of protocols somewhere alongside the protocol being developed. Some analysis efforts focus on the gap between specifications and implementations, and reviewing implementations is an important part of assessing that gap. Wood Expires 14 September 2023 [Page 8] Internet-Draft Formal Analysis Challenges March 2023 4. Document all known gaps between the protocol specification and known formal analysis. This helps ensure that the results of the analysis are properly represented to consumers of protocol specification documents. 5. Identify open issues or aspects of the protocol that require formal analysis during development of the protocol specification. One way to do this is to note that the entire draft is still a work in progress, whereas another way is to highlight specific properties of the protocol that require more analysis. Conversely, protocol designers and researchers can also take steps to bridge the gap between their skill set and the actual technical specifications. Some possible actions are below. 1. Collaborate with protocol document editors to determine what are ongoing analysis tasks. The end goal here is to minimize conflicts and competition that might emerge with different experts performing reviews. 2. Ensure that analysis work that requires running code, such as formal analyses using modeling tools such as ProVerif and Tamarin, are understandable and reproducible. It should be possible for any contributor in the IETF to re-run the analysis and understand its results. 5. Security Considerations This document discusses challenges for applying formal analysis to technical specifications produced by the IETF and IRTF. It does not raise new security considerations. 6. IANA Considerations This document has no IANA actions. 7. References 7.1. Normative References [RFC2119] Bradner, S., "Key words for use in RFCs to Indicate Requirement Levels", BCP 14, RFC 2119, DOI 10.17487/RFC2119, March 1997, . [RFC8174] Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174, May 2017, . Wood Expires 14 September 2023 [Page 9] Internet-Draft Formal Analysis Challenges March 2023 7.2. Informative References [MLS] Barnes, R., Beurdouche, B., Robert, R., Millican, J., Omara, E., and K. Cohn-Gordon, "The Messaging Layer Security (MLS) Protocol", Work in Progress, Internet- Draft, draft-ietf-mls-protocol-18, 13 March 2023, . [OHTTP] Thomson, M. and C. A. Wood, "Oblivious HTTP", Work in Progress, Internet-Draft, draft-ietf-ohai-ohttp-07, 9 March 2023, . [PRIVACYPASS] Davidson, A., Iyengar, J., and C. A. Wood, "The Privacy Pass Architecture", Work in Progress, Internet-Draft, draft-ietf-privacypass-architecture-11, 6 March 2023, . [ProVerif] Blanchet, B., "Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif", Foundations and TrendsĀ® in Privacy and Security vol. 1, no. 1-2, pp. 1-135, DOI 10.1561/3300000004, 2016, . [QUIC] Iyengar, J., Ed. and M. Thomson, Ed., "QUIC: A UDP-Based Multiplexed and Secure Transport", RFC 9000, DOI 10.17487/RFC9000, May 2021, . [RFC9000] Iyengar, J., Ed. and M. Thomson, Ed., "QUIC: A UDP-Based Multiplexed and Secure Transport", RFC 9000, DOI 10.17487/RFC9000, May 2021, . [Tamarin] Cortier, V., Delaune, S., Dreier, J., and E. Klein, "Automatic generation of sources lemmas in Tamarin: Towards automatic proofs of security protocols1", Journal of Computer Security vol. 30, no. 4, pp. 573-598, DOI 10.3233/jcs-210053, August 2022, . [TLS13] Rescorla, E., "The Transport Layer Security (TLS) Protocol Version 1.3", RFC 8446, DOI 10.17487/RFC8446, August 2018, . Wood Expires 14 September 2023 [Page 10] Internet-Draft Formal Analysis Challenges March 2023 Acknowledgments This document was influenced by conversations with many people that led to the UFMRG formation. Author's Address Christopher A. Wood Cloudflare Email: caw@heapingbits.net Wood Expires 14 September 2023 [Page 11]