Internet DRAFT - draft-analysis-challenges
draft-analysis-challenges
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,
<https://www.rfc-editor.org/rfc/rfc2119>.
[RFC8174] Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC
2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174,
May 2017, <https://www.rfc-editor.org/rfc/rfc8174>.
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,
<https://datatracker.ietf.org/doc/html/draft-ietf-mls-
protocol-18>.
[OHTTP] Thomson, M. and C. A. Wood, "Oblivious HTTP", Work in
Progress, Internet-Draft, draft-ietf-ohai-ohttp-07, 9
March 2023, <https://datatracker.ietf.org/doc/html/draft-
ietf-ohai-ohttp-07>.
[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,
<https://datatracker.ietf.org/doc/html/draft-ietf-
privacypass-architecture-11>.
[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,
<https://doi.org/10.1561/3300000004>.
[QUIC] Iyengar, J., Ed. and M. Thomson, Ed., "QUIC: A UDP-Based
Multiplexed and Secure Transport", RFC 9000,
DOI 10.17487/RFC9000, May 2021,
<https://www.rfc-editor.org/rfc/rfc9000>.
[RFC9000] Iyengar, J., Ed. and M. Thomson, Ed., "QUIC: A UDP-Based
Multiplexed and Secure Transport", RFC 9000,
DOI 10.17487/RFC9000, May 2021,
<https://www.rfc-editor.org/rfc/rfc9000>.
[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,
<https://doi.org/10.3233/jcs-210053>.
[TLS13] Rescorla, E., "The Transport Layer Security (TLS) Protocol
Version 1.3", RFC 8446, DOI 10.17487/RFC8446, August 2018,
<https://www.rfc-editor.org/rfc/rfc8446>.
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]
