You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Edinburgh » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Edinburgh

Return to search Previous output Next output

Output 151 of 401 in the submission

Output title

Extracting and verifying cryptographic models from C protocol code by symbolic execution

Type

E - Conference contribution

DOI

10.1145/2046707.2046745

Name of conference/published proceedings

Proceedings of the 18th ACM conference on Computer and communications security

Volume number

Issue number

First page of article

331

ISSN of proceedings

Year of publication

2011

URL

http://dl.acm.org/citation.cfm?doid=2046707.2046745

Number of additional authors

Additional information

<10> Originality: The results in this paper provide the first computationally sound verification of weak secrecy and authentication for (single execution paths of) cryptographic code in C code.

Significance: All prior work on verifying cryptographic code in C requires many manual annotations; our method is automatic, and helps find bugs quickly; several unknown bugs were discovered. Follow on work verifies 3000 LOC, more than any other method for this problem. Download http://research.microsoft.com/en-us/projects/csec/

Rigour: The paper includes formal correctness proofs, and also evaluation of the method on about 2000 LOC of examples. Acceptance rate of CCS 2011 is 14%.

Interdisciplinary

Cross-referral requested

Research group

F - Laboratory for Foundations of Computer Science

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract