liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Analysing TLS Implementations Using Full-Message Symbolic Execution
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering. Sectra Communications, Linköping, Sweden.ORCID iD: 0000-0002-3055-9951
Linköping University, Department of Computer and Information Science, Software and Systems. Linköping University, Faculty of Science & Engineering.ORCID iD: 0000-0003-1916-3398
2025 (English)In: Secure IT Systems: 29th Nordic Conference, NordSec 2024 Karlstad, Sweden, November 6–7, 2024 Proceedings / [ed] Leonardo Horn Iwaya, Liina Kamm, Leonardo Martucci, Tobias Pulls, Springer, 2025, Vol. 15396, p. 283-302Conference paper, Published paper (Refereed)
Abstract [en]

In this paper, we present a methodology for performing thorough analysis of TLS protocol implementations using dynamic symbolic execution. This method explores all possible inputs by treating entire messages as symbolic using KLEE. We are able to analyse the message parsing logic in detail, showing fulfilment of requirements from the protocol specification. This has previously not been performed for whole messages in complex protocols such as TLS. We tackle several problems that cause state space explosion by providing appropriate abstractions of implementation primitives. Additionally, we explore how protocol design choices impact the feasibility of analysis and argue for a strict TLS specification. We have applied our method to the ServerHello message parsing in several versions of the WolfSSL TLS 1.3 implementation. Our analysis revealed two vulnerabilities in the client implementation which were both assigned CVEs, one of them marked as high severity.

Place, publisher, year, edition, pages
Springer, 2025. Vol. 15396, p. 283-302
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 15396
Keywords [en]
Dynamic Symbolic Execution; Program Analysis; Protocol Analysis; Transport Layer Security
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-211257DOI: 10.1007/978-3-031-79007-2_15ISBN: 9783031790065 (print)ISBN: 9783031790072 (print)OAI: oai:DiVA.org:liu-211257DiVA, id: diva2:1932954
Conference
29th Nordic Conference, NordSec 2024 Karlstad, Sweden, November 6–7, 2024
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)Available from: 2025-01-30 Created: 2025-01-30 Last updated: 2025-01-30
In thesis
1. Towards Practical Formal Verification of Cryptographic Protocol Specifications and Implementations
Open this publication in new window or tab >>Towards Practical Formal Verification of Cryptographic Protocol Specifications and Implementations
2025 (English)Licentiate thesis, comprehensive summary (Other academic)
Abstract [en]

Modern computer systems communicate using protocols. Protocols are critical to security as they are the interface over which systems are accessible to the outside world. Cryptography is what enables secure communication even over insecure channels, and cryptographic protocols are the basis for modern internet security. Encryption enables confidentiality even if eavesdropping is possible, and cryptographic signatures can provide authenticity even if messages can be mimicked, modified, or reproduced.

Designing secure cryptographic protocols remains challenging. Many protocols once believed to be secure have since been broken and redesigned. The highest guarantees of security are achieved using formal methods, where mathematical logic is used for reasoning. Modern formal methods research tools have proven effective in finding and proving the absence of flaws in protocols, yet they are challenging to use. Correctly implementing large, complex protocols is also a challenge, and many vulnerabilities have been caused by errors introduced during the implementation phase. Formal software verification remains a daunting task which often requires manual effort by formal methods experts.

This licentiate thesis contributes towards providing formal protocol analysis methods that are intended to be more practical and useful for industrial application. Both the design phase of protocols and the analysis of protocol implementations are covered, showing how modern tools can be used to perform thorough analysis. The analysis discovers design and implementation flaws in modern commercial cryptographic protocols which are reported to the developers.

The analysis demonstrates challenges as well as the opportunities of adopting more formal methods for the analysis of protocols. Challenges which are tackled in this thesis include specifying an accurate model and selecting security properties for remote attestation proto-cols, and circumventing state space explosion during symbolic execution of protocol implementations. Opportunities include the ability to provide a more thorough analysis of protocol specifications as well as implementations in order to cover requirements which are difficult to test.

To make verification goals and assumptions more clear, this thesis also presents precise formulations of authentication which are appropriate for verification in the formal model. The authentication properties are suitable for protocols which perform one-way authentication of one of the agents, and complement existing mutual authentication definitions.

Place, publisher, year, edition, pages
Linköping: Linköping University Electronic Press, 2025. p. 31
Series
Linköping Studies in Science and Technology. Licentiate Thesis, ISSN 0280-7971 ; 2011
National Category
Computer Systems
Identifiers
urn:nbn:se:liu:diva-211228 (URN)10.3384/9789180759632 (DOI)9789180759625 (ISBN)9789180759632 (ISBN)
Presentation
2025-02-28, Ada Lovelace, B-building, Campus Valla, Linköping, 13:15 (English)
Opponent
Supervisors
Note

Funding: This work was partially supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.

Available from: 2025-01-28 Created: 2025-01-28 Last updated: 2025-01-30Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records

Wilson, JohannesAsplund, Mikael

Search in DiVA

By author/editor
Wilson, JohannesAsplund, Mikael
By organisation
Software and SystemsFaculty of Science & Engineering
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 63 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf