A Usable Formal Methods Sample Problem from TEEP
draft-mt-ufmrg-teep-sample-01
| Document | Type | Active Internet-Draft (individual) | |
|---|---|---|---|
| Authors | Cory Myers , Hannes Tschofenig | ||
| Last updated | 2023-11-05 | ||
| RFC stream | (None) | ||
| Intended RFC status | (None) | ||
| Formats | |||
| Stream | Stream state | (No stream defined) | |
| Consensus boilerplate | Unknown | ||
| RFC Editor Note | (None) | ||
| IESG | IESG state | I-D Exists | |
| Telechat date | (None) | ||
| Responsible AD | (None) | ||
| Send notices to | (None) |
draft-mt-ufmrg-teep-sample-01
Usable Formal Methods Proposed Research Group C. Myers
Internet-Draft
Intended status: Informational H. Tschofenig
Expires: 8 May 2024 5 November 2023
A Usable Formal Methods Sample Problem from TEEP
draft-mt-ufmrg-teep-sample-01
Abstract
This draft follows the invitation of [I-D.farrell-ufmrg-sample] to
propose another sample problem for demonstration, training, and
evaluation of formal methods in IETF work. It draws on recent work
from the Software Updates for the Internet of Things [suit] and
Trusted Execution Environment Provisioning [teep] working groups to
define a sample modeling problem for a novel rather than a familiar
IETF protocol.
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-mt-ufmrg-teep-sample/.
Discussion of this document takes place on the Usable Formal Methods
Research Group mailing list (mailto:ufmrg@irtf.org), which is
archived at https://mailarchive.ietf.org/arch/browse/ufmrg.
Subscribe at https://www.ietf.org/mailman/listinfo/ufmrg/.
Source for this draft and an issue tracker can be found at
https://github.com/cfm/draft-mt-ufmrg-teep-sample.
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."
Myers & Tschofenig Expires 8 May 2024 [Page 1]
Internet-Draft TEEP Sample November 2023
This Internet-Draft will expire on 8 May 2024.
Copyright Notice
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.
Table of Contents
1. Introduction . . . . . . . . . . . . . . . . . . . . . . . . 2
2. Conventions and Definitions . . . . . . . . . . . . . . . . . 3
3. The Trusted Execution Environment Provisioning (TEEP)
Protocol . . . . . . . . . . . . . . . . . . . . . . . . 3
3.1. NonceRequest/NonceRespone . . . . . . . . . . . . . . . . 4
3.2. QueryRequest . . . . . . . . . . . . . . . . . . . . . . 4
3.3. EvidenceRequest/EvidenceResponse . . . . . . . . . . . . 5
3.4. QueryResponse . . . . . . . . . . . . . . . . . . . . . . 5
3.5. SoftwareUpdate . . . . . . . . . . . . . . . . . . . . . 5
3.6. Update . . . . . . . . . . . . . . . . . . . . . . . . . 6
3.7. Success . . . . . . . . . . . . . . . . . . . . . . . . . 6
3.8. Security Properties . . . . . . . . . . . . . . . . . . . 6
4. Security Considerations . . . . . . . . . . . . . . . . . . . 7
5. IANA Considerations . . . . . . . . . . . . . . . . . . . . . 7
6. References . . . . . . . . . . . . . . . . . . . . . . . . . 7
6.1. Normative References . . . . . . . . . . . . . . . . . . 7
6.2. Informative References . . . . . . . . . . . . . . . . . 8
Authors' Addresses . . . . . . . . . . . . . . . . . . . . . . . 9
1. Introduction
In this draft we take the Trusted Execution Environment Provisioning
protocol [I-D.ietf-teep-protocol] to be a good domain from which to
draw a sample modeling problem for slightly different reasons than
those proposed in [I-D.farrell-ufmrg-sample].
1. TEEP is a proposed standard under active development, at working-
group consensus as of this writing. Formal modeling, even for
demonstration or training purposes, can therefore increase
familiarity with the TEEP protocol, including outside of the SUIT
and TEEP working groups directly involed in its development.
Myers & Tschofenig Expires 8 May 2024 [Page 2]
Internet-Draft TEEP Sample November 2023
2. The TEEP protocol is expressly concerned with security, so it has
security properties amenable to formal description, modeling, and
analysis. Any findings may have valuable security implications.
3. The TEEP protocol has well-defined use cases and includes a
number of options for flexibility, including provisions for
constrained environments. Modeling the entire protocol,
including all its options, is a reasonable challenge for a
learning or training exercise. By contrast,
[I-D.farrell-ufmrg-sample] limits itself to just the SEARCH
command of [RFC9051].
4. The TEEP protocol follows a typical protocol design in the IETF
where various already-standardized technologies are reused. In
this case, protocols from the Software Updates for Internet of
Things (SUIT) architecture [RFC9019] and the Remote Attestation
Procedures (RATS) architecture [RFC9334] are incorporated into
the design.
5. The architecture of the TEEP protocol is also representative for
IETF protocol development since more than two parties are
involved in the protocol communication even in a single, self-
contined deployment. Whether a formal model must consider all
parties or can limit itself to a subset is a worthwhile question
about the scope of this sample problem.
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. The Trusted Execution Environment Provisioning (TEEP) Protocol
The Trusted Execution Environment Provisioning protocol
[I-D.ietf-teep-protocol] specifies communication between a Trusted
Application Manager (TAM) [RFC9397] (Section 2) and a TEEP Agent.
Importantly, this communication is relayed by an _untrusted_ TEEP
Broker [RFC9397] (Section 6.1). Two security-sensitive payloads are
communicated via the TEEP protocol, namely:
* Trusted Applications (TAs) and Trusted Components (TCs) [RFC9397]
(Section 2); and
* attestation evidence.
Myers & Tschofenig Expires 8 May 2024 [Page 3]
Internet-Draft TEEP Sample November 2023
A Trusted Application is an application (or, in some implementations,
an application component) that runs in a TEE.
A Trusted Component is a set of code and/or data in a TEE that is
managed as a unit by a TAM. Trusted Applications and Personalization
Data [RFC9397] (Section 2) are thus managed by being included in
Trusted Components.
TCs are provided by developers or authors, which TEEP calls "Trusted
Component Signers" [RFC9397] (Section 2). SUIT manifests protect
TCs' integrity and may optionally protect their confidentiality as
well. Neither the TAM nor the TEEP Broker should be able to modify
TCs. TEEP Agents only install TCs from sources they trust.
Attestation evidence is typically communicated from the TEEP Agent to
the TAM, although there is the option to offer attestation
capabilities in both directions. In the description below, we focus
only on attestation of the Device [RFC9397] (Section 2) containing
the TEEP Agent to the TAM, rather than attestation in the other
direction.
The description below illustrates the basic communication
interaction, with details of the TEEP protocol abstracted away.
3.1. NonceRequest/NonceRespone
TAM -> Verifier: NonceRequest
TAM <- Verifier: NonceResponse
Nonce
3.2. QueryRequest
TAM -> TEEP Agent: QueryRequest
{token, challenge, supported-teep-cipher-suites,
supported-suit-cose-profiles, data-item-requested(trusted-components,
attestation)}SK_TAM
* The challenge is a random number provided by the Verifier
[RFC9334] (Section 1). It is used to demonstrate the freshness of
the attestation evidence.
* The token is a random number that is used to match the
QueryRequest against the QueryResponse.
* supported-teep-cipher-suites and supported-suit-cose-profiles
offer cipher-suite negotation.
Myers & Tschofenig Expires 8 May 2024 [Page 4]
Internet-Draft TEEP Sample November 2023
* data-item-requested(X) indicates the functionality that the TAM
requests the TEEP Agent perform.
* {_}SK_TAM indicates a digital signature over the payload of the
message using a private (or secret) key that is only known to the
TAM.
3.3. EvidenceRequest/EvidenceResponse
TEEP Agent -> Attester: EvidenceRequest
challenge
TEEP Agent <- Attester: EvidenceResponse
{challenge, claims}SK_ATTESTER
* {challenge, claims}SK_ATTESTER represents the evidence, which is
signed by the Attester using its private key SK_ATTESTER.
In addition to the inclusion of the Challenge, the random number
provided by the Verifier, it also includes further (unspecified)
claims. While those claims are important for the overall system,
they are not in scope of this analysis.
3.4. QueryResponse
TAM <- TEEP Agent: QueryResponse
{token, selected-teep-cipher-suite, attestation-payload-format(EAT),
attestation-payload({challenge, claims}SK_ATTESTER), tc-list}SK_AGENT
* selected-teep-cipher-suite indicates the selected cipher suite.
* attestation-payload-format(EAT) indicates the format of the
attached attestation evidence.
* tc-list conveys the list of Trusted Components installed on the
Device.
* attestation-payload(_) contains the evidence provided by the
Attester in the previous step.
* {_}SK_AGENT indicates a digital signature over the payload of the
message using a private (or secret) key that is only known to the
Agent.
3.5. SoftwareUpdate
Author -> TAM: SoftwareUpdate
{manifest, sequence_nr, TC}SK_AUTHOR
Myers & Tschofenig Expires 8 May 2024 [Page 5]
Internet-Draft TEEP Sample November 2023
* The manifest contains instructions for how to install the
software.
* sequence_nr, as the name indicates, allows the TEEP Agent to
distingush this update from earlier versions of the software.
* TC is the Trusted Component to be installed. This could be a
binary, configuration data, or both.
* {_}SK_AUTHOR indicates a digital signature over the payload of the
message using a private (or secret) key that is only known to the
author, i.e. the Trusted Component Signer.
3.6. Update
The TAM transmits an update to the TEEP Agent containing the
previously obtained payload provided by the author.
TAM -> TEEP Agent: Update
{token2, {manifest, sequence_nr, software}SK_AUTHOR}SK_TAM
* token2 is a new random number, which is again used by the TAM to
match requests against responses.
* {_}SK_TAM indicates a digital signature over the payload of the
message using a private (or secret) key that is only known to the
TAM.
3.7. Success
The TEEP Agent returns this message when the software installation
was successful.
TAM <- TEEP Agent: Success
{token2}SK_AGENT
* {_}SK_AGENT indicates a digital signature over the payload of the
message using a private (or secret) key that is only known to the
Agent.
3.8. Security Properties
In addition to the integrity and authentication properties, an
important aspect is replay protection.
At the [suit-interim] meeting, the following editorial addition was
proposed [thaler] in TEEP's security consideration (Section 10 of
[I-D.ietf-teep-protocol]):
Myers & Tschofenig Expires 8 May 2024 [Page 6]
Internet-Draft TEEP Sample November 2023
The TEEP protocol supports replay protection as follows. The
transport protocol under the TEEP protocol might provide replay
protection, but may be terminated in the TEEP Broker which is not
trusted by the TEEP Agent and so the TEEP protocol does replay
protection itself. If attestation of the TAM is used, the
attestation freshness mechanism provides replay protection for
attested QueryRequest messages. If non-attested QueryRequest
messages are replayed, the TEEP Agent will generate QueryResponse
or Error messages, but the REE can already conduct Denial of
Service attacks against the TEE and/or the TAM even without the
TEEP protocol. QueryResponse messages have replay protection via
attestation freshness mechanism, or the token field in the message
if attestation is not used. Update messages have replay
protection via the suit-manifest-sequence-number (see
Section 8.4.2 of [I-D.ietf-suit-manifest]). Error and Success
messages have replay protection via SUIT Reports and/or the token
field in the message, where a TAM can detect which message it is
in response to.
Any formal model of TEEP should be able to prove this replay
protection.
While confidentiality protection is possible for attestation evidence
as well as for Trusted Components, it is not mandatory functionality.
4. Security Considerations
This document has no security considerations of its own, although it
may contribute indirectly to the development of new security
considerations for the TEEP protocol.
5. IANA Considerations
This document has no IANA actions.
6. References
6.1. Normative References
[I-D.ietf-teep-protocol]
Tschofenig, H., Pei, M., Wheeler, D. M., Thaler, D., and
A. Tsukamoto, "Trusted Execution Environment Provisioning
(TEEP) Protocol", Work in Progress, Internet-Draft, draft-
ietf-teep-protocol-17, 23 October 2023,
<https://datatracker.ietf.org/doc/html/draft-ietf-teep-
protocol-17>.
Myers & Tschofenig Expires 8 May 2024 [Page 7]
Internet-Draft TEEP Sample November 2023
[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>.
[RFC9019] Moran, B., Tschofenig, H., Brown, D., and M. Meriac, "A
Firmware Update Architecture for Internet of Things",
RFC 9019, DOI 10.17487/RFC9019, April 2021,
<https://www.rfc-editor.org/rfc/rfc9019>.
[RFC9334] Birkholz, H., Thaler, D., Richardson, M., Smith, N., and
W. Pan, "Remote ATtestation procedureS (RATS)
Architecture", RFC 9334, DOI 10.17487/RFC9334, January
2023, <https://www.rfc-editor.org/rfc/rfc9334>.
6.2. Informative References
[I-D.farrell-ufmrg-sample]
Farrell, S., "Usable Formal Methods Research Group Sample
Problems", Work in Progress, Internet-Draft, draft-
farrell-ufmrg-sample-00, 19 June 2023,
<https://datatracker.ietf.org/doc/html/draft-farrell-
ufmrg-sample-00>.
[RFC9051] Melnikov, A., Ed. and B. Leiba, Ed., "Internet Message
Access Protocol (IMAP) - Version 4rev2", RFC 9051,
DOI 10.17487/RFC9051, August 2021,
<https://www.rfc-editor.org/rfc/rfc9051>.
[RFC9397] Pei, M., Tschofenig, H., Thaler, D., and D. Wheeler,
"Trusted Execution Environment Provisioning (TEEP)
Architecture", RFC 9397, DOI 10.17487/RFC9397, July 2023,
<https://www.rfc-editor.org/rfc/rfc9397>.
[suit] IETF, "Software Updates for the Internet of Things", 2023,
<https://datatracker.ietf.org/wg/suit/about/>.
[suit-interim]
Thaler, D., "interim-2023-suit-01", 11 September 2023,
<https://datatracker.ietf.org/doc/agenda-interim-2023-
suit-01-sessa/>.
[teep] IETF, "Trusted Execution Environment Provisioning", 2023,
<https://datatracker.ietf.org/wg/teep/about/>.
Myers & Tschofenig Expires 8 May 2024 [Page 8]
Internet-Draft TEEP Sample November 2023
[thaler] Thaler, D., "TEEP Protocol: draft-ietf-teep-protocol-16",
11 September 2023, <https://datatracker.ietf.org/meeting/
interim-2023-suit-01/materials/slides-interim-2023-suit-
01-sessa-teep-protocol-00.pdf>.
Authors' Addresses
Cory Myers
Email: cfm@acm.org
Hannes Tschofenig
Email: hannes.tschofenig@gmx.net
Myers & Tschofenig Expires 8 May 2024 [Page 9]