Markdown Version | Session Recording

Session Date/Time: 24 Jul 2025 12:30

ufmrg

Summary

The ufmrg meeting featured two presentations. The first, by Saba, covered the topic of tested TLS, focusing on attestation and its integration with TLS. The discussion included threat models, security goals, and potential solutions, including post-handshake attestation. The second presentation, by Tahina, detailed the EmerPers project, which focuses on verified parsing and serialization of binary data formats, highlighting its application in HyperV network virtualization and exploring the use of AI in specification generation.

Key Discussion Points

• Tested TLS and Attestation:
  • The initial proposal for tested TLS involved integrating attestation within the TLS handshake.
  • Formal analysis revealed that this approach breaks server authentication due to the removal of the long-term key.
  • The need for a realistic threat model for confidential computing was emphasized, as current cloud service provider models are often inadequate.
  • Post-handshake attestation based on RFC 9261 was proposed as a more suitable solution.
  • The importance of binding evidence to the TLS session was discussed, ensuring that attestation data cannot be reused across sessions.
• EmerPers and Verified Parsing:
  • The project aims to provide formally verified parsing and serialization of binary data formats, mitigating security vulnerabilities.
  • EmerPers has been successfully deployed in HyperV network virtualization, verifying packet validators.
  • The 3D language is used for describing data formats, augmented with value constraints and variable language structures.
  • AI is being explored to generate data format descriptions from RFCs, with human review remaining essential.
  • The benefits of having formal specifications within RFCs were discussed.
  • Discussion of current LLMs and their hallucinations, and suggestions of new models, such as feeding the LLM .3D files and having it create a spec.
• General:
  • The challenges of balancing security with protocol ossification were mentioned in the context of TCP options.
  • The usability barriers and accessibility of formal methods tools were acknowledged as areas requiring improvement.
  • The importance of the UFMRG in promoting the adoption of formal data description languages and tools was highlighted.
  • Discussions around how to handle discrepancies between English and Formula specifications and how to treat this as an errata.

Decisions and Action Items

N/A

Next Steps

• Continue the formal modeling of the post-handshake attestation proposal.
• Work toward making formal methods more accessible to designers.
• Improve readability of generated types from CDDL in EmerPers.
• Promote adoption of data format specifications in RFCs.
• Follow-up discussion regarding the expath list regarding to the Atosama BOFF.