CAOVerif: An open-source deductive verification platform for cryptographic software implementations

被引：1

作者：

Almeida, Jose Bacelar ^{[1
,2
]}

Barbosa, Manuel ^{[1
,2
]}

Filliatre, Jean-Christophe ^{[3
,4
]}

Pinto, Jorge Sousa ^{[1
,2
]}

Vieira, Barbara ^{[1
,2
]}

机构：

[1] HASLab INESC TEC, Braga, Portugal

[2] Univ Minho, Braga, Portugal

[3] INRIA Saclay Ile de France, ProVal, Orsay, France

[4] Univ Paris 11, CNRS, LRI, F-91405 Orsay, France

来源：

SCIENCE OF COMPUTER PROGRAMMING | 2014年 / 91卷

关键词：

Formal verification; Program verification; Cryptographic software; Deductive verification; CERTIFICATION; SECURITY; SYSTEM; PROVER; TOOL;

D O I：

10.1016/j.scico.2012.09.019

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

CAO is a domain-specific imperative language for cryptography, offering a rich mathematical type system and crypto-oriented language constructions. We describe the design and implementation of a deductive verification platform for CAO and demonstrate that the development time of such a complex verification tool could be greatly reduced by building on the Jessie plug-in included in the Frama-C framework. We discuss the interesting challenges raised by the domain-specific characteristics of CAO, and describe how we tackle these problems in our design. We base our presentation on real-world examples of CAO code, extracted from the open-source code of the NaCl cryptographic library, and illustrate how various cryptography-relevant security properties can be verified. (C) 2012 Elsevier B.V. All rights reserved.

引用

页码：216 / 233

页数：18

共 50 条

[1] Deductive verification of cryptographic software
Almeida, Jose Bacelar
Barbosa, Manuel
Pinto, Jorge Sousa
Vieira, Barbara
INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2010, 6 (03) : 203 - 218
[2] A Tertiary Study on Open-Source Software Research
Imtiaz, Saima
Imtiaz, Salma
Almadhor, Ahmad
Kulhanek, Rastislav
IEEE ACCESS, 2024, 12 : 189952 - 189993
[3] Evaluation indicators for open-source software: a review
Zhao, Yuhang
Liang, Ruigang
Chen, Xiang
Zou, Jing
CYBERSECURITY, 2021, 4 (01)
[4] The Role of Open-Source Software in the Energy Sector
Klimt, Jonathan
Eiling, Niklas
Wege, Felix
Baude, Jonas
Monti, Antonello
ENERGIES, 2023, 16 (16)
[5] Use of open-source software platform to develop dashboards for control and automation of flow chemistry equipment
van der Westhuizen, C. Johan
du Toit, Jurie
Neyt, Nicole
Riley, Darren
Panayides, Jenny-Lee
DIGITAL DISCOVERY, 2022, 1 (05): : 596 - 604
[6] The Phenobottle, an open-source photobioreactor platform for environmental simulation
Bates, Harvey
Zavafer, Alonso
Szabo, Milan
Ralph, Peter J.
ALGAL RESEARCH-BIOMASS BIOFUELS AND BIOPRODUCTS, 2020, 52
[7] SEcube™: An Open-Source Security Platform in a Single SoC
Varriale, Antonio
Vatajelu, Elena Ioana
Di Natale, Giorgio
Prinetto, Paolo
Trotta, Pascal
Margaria, Tiziana
2016 11TH IEEE INTERNATIONAL CONFERENCE ON DESIGN & TECHNOLOGY OF INTEGRATED SYSTEMS IN NANOSCALE ERA (DTIS), 2016,
[8] Total alkalinity measurement using an open-source platform
Sandborn, Daniel E. E.
Minor, Elizabeth C. C.
Hill, Craig
LIMNOLOGY AND OCEANOGRAPHY-METHODS, 2023, 21 (06): : 334 - 344
[9] Open-source software for automated rodent behavioral analysis
Isik, Sena
Unal, Gunes
FRONTIERS IN NEUROSCIENCE, 2023, 17
[10] The Prisoner's Dilemma of Open-Source Software Security
Koch, Christian
COMPUTER, 2024, 57 (10) : 82 - 85

← 1 2 3 4 5 →