The workshop explores the interplay between formal methods and trusted hardware, e.g., Trusted Execution Environments (TEEs) and Trusted Platform Module (TPMs).

Important dates:
- Paper submission: 28 July (extended)
- Notification: 11 August

Submission: https://easychair.org/conferences/?conf=pavetrust2024

Trusted Execution Environments (TEEs) are now commonplace with implementations like Intel SGX and AMD SEV widely available. This technology offers new guarantees, such as integrity and confidentiality for running applications, that are not typically available in (untrusted) conventional platforms. Therefore, TEEs are being rapidly adopted by security-focused companies intending to harden their systems to provide such guarantees.

This workshop intends to explore the interplay between TEE-based implementations of a Trusted Third Party (TTP) and program analysis and system verification. It should provide a venue where academics and practitioners interested in these topics come together to debate the connection between these two areas. We are especially interested in promoting:

  • (A) the application of formal methods, and more specifically of program analysis and system verification, to the specification and/or analysis of the trusted stack executing these TEE-hardened applications - this stack might include CPU microcode, firmware code, Operating System (OS) code, protocols for provisioning and attestation, and the application itself
  • (B) innovative applications of TEEs to execute formal methods technologies (such as program analysers/verifiers).

While the frameworks proposed in the context of (A) should help the adoption of TEE-based technologies by increasing the community’s confidence on the security of TEE-based systems, the applications arising in the context of (B) should introduce analysis frameworks that enjoy non-conventional properties such as confidentiality of the analysed systems and trustworthiness of the analysis outcome. It should be possible to deliver object code to users who know that the corresponding sources have passed agreed verification procedures, without the users seeing the sources or having to have trust in other parties.

Topics of interest

Topics of interest include but not limited to

  • Protocol analysis (e.g., attestation)
  • Trusted Execution Environment (TEE)
  • Trusted Platform Module (TPM)
  • Hardware Security Modules (HSM)
  • Trusted software (OS, firmware, etc.)
  • Security and privacy analysis
  • Case studies including trusted hardware
  • Standardization process
  • Usability of formal methods tools

Important dates

  • Paper submission: 28 July (extended)
  • Author Notification: 11 August
  • Final paper submission: 19 August
  • Workshop: 9 September

We invite the submissions on topics (A) and (B) above in the following formats:

  • Regular research papers (maximum of 6 pages, excluding well-marked references and appendices) presenting original work
  • Extended abstracts (maximum of 2 pages, excluding well-marked references and appendices) aimed at encouraging discussion and collaboration. Extended abstracts may summarize recently published research or outline new emerging ideas.

All submissions should be submitted as a PDF file generated using the two-column ACM acmart template available at https://www.acm.org/publications/proceedings-template, using the [sigconf,review] option. The accepted submissions will have to be presented, in-person, by one of the authors at the workshop.

Submission link: https://easychair.org/conferences/?conf=pavetrust2024

Publication

Submissions will go through a single-blind peer-reviewing process aimed at selecting the papers to be presented at the workshop, but also at providing detailed constructive feedback to authors. There are no formal workshop proceedings; the accepted papers and slides will only be made available to registered attendees in the workshop’s online repository. Any queries about the workshop should be addressed to workshop@tbtl.com.