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] Layout Verification Using Open-Source Software
Krinke, Andreas
Fischbach, Robert
Lienig, Jens
PROCEEDINGS OF THE 2024 INTERNATIONAL SYMPOSIUM ON PHYSICAL DESIGN, ISPD 2024, 2024, : 137 - 142
[3] Microgrid Planner: An Open-Source Software Platform
Reich, Daniel
Frye, Leah
INFORMS JOURNAL ON COMPUTING, 2024,
[4] An open-source cryptographic coprocessor
Gutmann, P
USENIX ASSOCIATION PROCEEDINGS OF THE NINTH USENIX SECURITY SYMPOSIUM, 2000, : 97 - 111
[5] An open-source platform for distributed Linux Software Routers
Bolla, Raffaele
Bruschi, Roberto
COMPUTER COMMUNICATIONS, 2013, 36 (04) : 396 - 410
[6] OpenVolcano: An Open-Source Software Platform for Fog Computing
Bruschi, R.
Lago, P.
Lamanna, G.
Lombardo, C.
Mangialardi, S.
2016 28TH INTERNATIONAL TELETRAFFIC CONGRESS (ITC 28), VOL 2, 2016, : 22 - 27
[7] EvaSIM: a Software Simulator for the EVA Open-source Robotics Platform
Da Rocha, Marcelo Marques
Cruz-Sandoval, Dagoberto
Favela, Jesus
Muchaluat-Saade, Debro C.
2022 31ST IEEE INTERNATIONAL CONFERENCE ON ROBOT AND HUMAN INTERACTIVE COMMUNICATION (IEEE RO-MAN 2022), 2022, : 714 - 721
[8] Open-source software platform for medical image segmentation applications
Namias, R.
D'Amato, J. P.
del Fresno, M.
13TH INTERNATIONAL CONFERENCE ON MEDICAL INFORMATION PROCESSING AND ANALYSIS, 2017, 10572
[9] Open-source data analysis and visualization software platform: SAGUARO
Kim, Dae Wook
Lewis, Benjamin J.
Burge, James H.
OPTICAL MANUFACTURING AND TESTING IX, 2011, 8126
[10] Development of an open-source software platform for conventional and particle therapy
Steininger, P.
Mehrwald, M.
Kellner, D.
Pinzger, M.
Mitterlechner, M.
Memelink, M.
Keuschnigg, P.
Boehler, A.
Sedlmayer, F.
Deutschmann, H.
RADIOTHERAPY AND ONCOLOGY, 2014, 111 : S121 - S121

← 1 2 3 4 5 →