Type checking cryptography implementations
2012 (English)In: Lecture Notes in Computer Science, Springer , 2012, Vol. 7141, 316-334 p.Conference paper (Refereed) Published
Cryptographic software development is a challenging field: high performance must be achieved, while ensuring correctness and compliance with low-level security policies. CAO is a domain specific language designed to assist development of cryptographic software. An important feature of this language is the design of a novel type system introducing native types such as predefined sized vectors, matrices and bit strings, residue classes modulo an integer, finite fields and finite field extensions, allowing for extensive static validation of source code. We present the formalisation, validation and implementation of this type system.
Place, publisher, year, edition, pages
Springer , 2012. Vol. 7141, 316-334 p.
Bit-strings, Cryptographic software, Domain specific languages, Finite fields, Formalisation, Residue class, Security policy, Source codes, Type systems, Typechecking
IdentifiersURN: urn:nbn:se:bth-7058DOI: 10.1007/978-3-642-29320-7_21Local ID: oai:bth.se:forskinfo2474A8502D95F042C1257AC900499A0EOAI: oai:DiVA.org:bth-7058DiVA: diva2:834637
4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011
Conference site: Tehran2012-12-212012-12-032015-06-30Bibliographically approved