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, . 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, . [RFC8174] Leiba, B., "Ambiguity of Uppercase vs Lowercase in RFC 2119 Key Words", BCP 14, RFC 8174, DOI 10.17487/RFC8174, May 2017, . [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, . [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, . 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, . [RFC9051] Melnikov, A., Ed. and B. Leiba, Ed., "Internet Message Access Protocol (IMAP) - Version 4rev2", RFC 9051, DOI 10.17487/RFC9051, August 2021, . [RFC9397] Pei, M., Tschofenig, H., Thaler, D., and D. Wheeler, "Trusted Execution Environment Provisioning (TEEP) Architecture", RFC 9397, DOI 10.17487/RFC9397, July 2023, . [suit] IETF, "Software Updates for the Internet of Things", 2023, . [suit-interim] Thaler, D., "interim-2023-suit-01", 11 September 2023, . [teep] IETF, "Trusted Execution Environment Provisioning", 2023, . 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, . Authors' Addresses Cory Myers Email: cfm@acm.org Hannes Tschofenig Email: hannes.tschofenig@gmx.net Myers & Tschofenig Expires 8 May 2024 [Page 9]