1. Signed Cryptographic Program Verification with Typed CryptoLine 2019 CCS FormalVerification
    Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang
    [View PDF on precision.moscito.org]
    [Show BibTex Citation]

    @inproceedings{Fu:2019:SCP:3319535.3354199,
    author = {Fu, Yu-Fu and Liu, Jiaxiang and Shi, Xiaomu and Tsai, Ming-Hsien and Wang, Bow-Yaw and Yang, Bo-Yin},
    title = {Signed Cryptographic Program Verification with Typed CryptoLine},
    booktitle = {Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security},
    series = {CCS '19},
    year = {2019},
    isbn = {978-1-4503-6747-9},
    location = {London, United Kingdom},
    pages = {1591--1606},
    numpages = {16},
    url = {http://doi.acm.org/10.1145/3319535.3354199},
    doi = {10.1145/3319535.3354199},
    acmid = {3354199},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {cryptographic programs, formal verification, model checking},
    }

We develop an automated formal technique to specify and verify signed computation in cryptographic programs. In addition to new instructions, we introduce a type system to detect type errors in programs. A type inference algorithm is also provided to deduce types and instruction variants in cryptographic programs. In order to verify signed cryptographic C programs, we develop a translator from the GCC intermediate representation to our language. Using our technique, we have verified 82 C functions in cryptography libraries including NaCl, wolfSSL, bitcoin, OpenSSL, and BoringSSL.

  1.