Detecting and Preventing Type flaws at Static Time

Chiara Bodei, Linda Brodo, Pierpaolo Degano, Han Gao

    Research output: Contribution to journalConference articleResearchpeer-review

    Abstract

    A type flaw attack on a security protocol is an attack where an honest principal is cheated on interpreting a field in a message as the one with a type other than the intended one. In this paper, we shall present an extension of the LYSA calculus to cope with types, by using tags to represent the intended types of terms. We develop a Control Flow Analysis for this calculus which soundly over-approximates all the possible behaviour of a protocol and, in particular, is able to capture any type confusion that may occur during the protocol execution. The analysis acts in a descriptive way: it describes which violations may occur. In the same setting, our approach also offers a prescriptive usage: we can impose a type discipline, by forcing some data to be of the expected types. At this point, the analysis may statically check that type violations are not possible any longer. In other words, we instrument the code with the only checks necessary to enforce type security. Finally, we apply our framework to a multi-protocol setting, where the risk of having type flaw attacks is higher. Our analysis has been implemented and successfully applied to a number of security protocols, showing it is able to capture type flaw attacks. The implementation complexity of the analysis is low polynomial.
    Original languageEnglish
    JournalJournal of Computer Security
    Volume18
    Issue number2
    Pages (from-to)229-264
    ISSN0926-227X
    DOIs
    Publication statusPublished - 2010
    EventInternational Workshop on Issues in the Theory of Security - Braga, Portugal
    Duration: 1 Jan 2007 → …

    Conference

    ConferenceInternational Workshop on Issues in the Theory of Security
    CityBraga, Portugal
    Period01/01/2007 → …

    Fingerprint Dive into the research topics of 'Detecting and Preventing Type flaws at Static Time'. Together they form a unique fingerprint.

    Cite this