Automated Verification of Real-World Cryptographic Implementations

被引：12
|
作者：
Tomb, Aaron [1 ]
机构：
[1] Galois, Xanthi, Greece
来源：
IEEE SECURITY & PRIVACY | 2016年 / 14卷 / 06期
关键词：
correctness proofs; cryptography; privacy; program verification; security; software engineering;
D O I：
10.1109/MSP.2016.125
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Cryptographic software is increasingly important but notoriously difficult to implement correctly. The open source Cryptol and Software Analysis Workbench tools can automatically and rigorously prove equivalence between machine-readable cryptographic specifications and real-world implementations.
引用
收藏
页码：26 / 33
页数：8
相关论文
共 50 条
  • [1] Automated Verification Of Cryptographic Protocol Implementations
    Babenko, Liudmila
    Pisarev, Ilya
    12TH INTERNATIONAL CONFERENCE ON THE DEVELOPMENTS IN ESYSTEMS ENGINEERING (DESE 2019), 2019, : 849 - 854
  • [2] Tamarin: Verification of Large-Scale, Real-World, Cryptographic Protocols
    Basin, David
    Cremers, Cas
    Dreier, Jannik
    Sasse, Ralf
    IEEE SECURITY & PRIVACY, 2022, 20 (03) : 24 - 32
  • [3] Verification of Implementations of Cryptographic Hash Functions
    Wang, Dexi
    Jiang, Yu
    Song, Houbing
    He, Fei
    Gu, Ming
    Sun, Jiaguang
    IEEE ACCESS, 2017, 5 : 7816 - 7825
  • [4] Probabilistic Relational Verification for Cryptographic Implementations
    Barthe, Gilles
    Fournet, Cedric
    Gregoire, Benjamin
    Strub, Pierre-Yves
    Swamy, Nikhil
    Zanella-Beguelin, Santiago
    ACM SIGPLAN NOTICES, 2014, 49 (01) : 193 - 205
  • [5] Vivienne: Relational Verification of Cryptographic Implementations in WebAssembly
    Tsoupidi, Rodothea Myrsini
    Balliu, Musard
    Baudry, Benoit
    2021 IEEE SECURE DEVELOPMENT CONFERENCE (SECDEV 2021), 2021, : 94 - 102
  • [6] INRiM solutions for QKD real-world network implementations
    Virzi, Salvatore
    Meda, Alice
    Clivati, Cecilia
    Bertaina, Gianluca
    Donadello, Simone
    Gramegna, Marco
    Degiovanni, Ivo Pietro
    Genovese, Marco
    Calonico, Davide
    2024 24TH INTERNATIONAL CONFERENCE ON TRANSPARENT OPTICAL NETWORKS, ICTON 2024, 2024,
  • [7] miTLS: Verifying Protocol Implementations against Real-World Attacks
    Bhargavan, Karthikeyan
    Fournet, Cedric
    Kohlweiss, Markulf
    IEEE SECURITY & PRIVACY, 2016, 14 (06) : 18 - 25
  • [8] Offline Signature Verification on Real-World Documents
    Engin, Deniz
    Kantarci, Alperen
    Arslan, Secil
    Ekenel, Hazim Kemal
    2020 IEEE/CVF CONFERENCE ON COMPUTER VISION AND PATTERN RECOGNITION WORKSHOPS (CVPRW 2020), 2020, : 3518 - 3526
  • [9] FORMAL VERIFICATION - IS IT PRACTICAL FOR REAL-WORLD DESIGN
    CAMURATI, P
    CHIN, SK
    FOURMAN, M
    PRINETTO, P
    TAKAHARA, A
    IEEE DESIGN & TEST OF COMPUTERS, 1989, 6 (06): : 50 - 58
  • [10] Linear lower bounds on real-world implementations of concurrent objects
    Fich, FE
    Hendler, D
    Shavit, N
    46TH ANNUAL IEEE SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 2005, : 165 - 173
12345