CISPA
Browse
cispa_all_3309.pdf (512.99 kB)

Modular Black-box Runtime Verification of Security Protocols

Download (512.99 kB)
conference contribution
posted on 2023-11-29, 18:14 authored by Kevin MorioKevin Morio, Dennis Jackson, Marco Vassena, Robert KünnemannRobert Künnemann
Verification techniques have been applied to the design of secure protocols for decades. However, relatively few efforts have been made to ensure that verified designs are also implemented securely. Static code verification techniques offer one way to bridge the verification gap between design and implementation, but require substantial expertise and manual labor to realize in practice. In this short paper, we propose black-box runtime verification as an alternative approach to extend the security guarantees of protocol designs to their implementations. Instead of instrumenting the complete protocol implementation, our approach only requires instrumenting common cryptographic libraries and network interfaces with a runtime monitor that is automatically synthesized from the protocol specification. This lightweight technique allows the effort for instrumentation to be shared among different protocols and ensures security with presumably minimal performance overhead.

History

Preferred Citation

Kevin Morio, Dennis Jackson, Marco Vassena and Robert Künnemann. Modular Black-box Runtime Verification of Security Protocols. In: Workshop on Programming Languages and Analysis for Security (PLAS). 2020.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Workshop on Programming Languages and Analysis for Security (PLAS)

Legacy Posted Date

2020-12-01

Open Access Type

  • Gold

BibTeX

@inproceedings{cispa_all_3309, title = "Modular Black-box Runtime Verification of Security Protocols", author = "Morio, Kevin and Jackson, Dennis and Vassena, Marco and Künnemann, Robert", booktitle="{Workshop on Programming Languages and Analysis for Security (PLAS)}", year="2020", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC