| Internet-Draft | Formal Analysis Challenges | March 2023 |
| Wood | Expires 14 September 2023 | [Page] |
This document discusses challenges, opportunities, and directions for formal analysis of protocols developed in the IETF.¶
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.¶
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 (c) 2023 IETF Trust and the persons identified as the document authors. All rights reserved.¶
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.¶
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.¶
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:¶
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.¶
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.¶
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:¶
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.¶
This section describes some high level problems that impact the scale at which the IETF and IRTF applies formal analysis to technical specifications.¶
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.¶
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.¶
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.¶
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.¶
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.¶
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.¶
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.¶
This document discusses challenges for applying formal analysis to technical specifications produced by the IETF and IRTF. It does not raise new security considerations.¶
This document has no IANA actions.¶
This document was influenced by conversations with many people that led to the UFMRG formation.¶