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 条

[31] Decision support in engineering design: the ELIGERE open source software platform
Grazioso, Stanislao
Caporaso, Teodorico
Di Gironimo, Giuseppe
INTERNATIONAL JOURNAL OF INTERACTIVE DESIGN AND MANUFACTURING - IJIDEM, 2024, 18 (01): : 509 - 524
[32] Open-Source Software Defined Networking Controllers: State-of-the-Art, Challenges and Solutions for Future Network Providers
Rahim, Johari Abdul
Nordin, Rosdiadee
Amodu, Oluwatosin Ahmed
CMC-COMPUTERS MATERIALS & CONTINUA, 2024, 80 (01): : 747 - 800
[33] Leaf: An open-source cybersecurity training platform for realistic edge-IoT scenarios
Ficco, Massimo
Palmieri, Francesco
JOURNAL OF SYSTEMS ARCHITECTURE, 2019, 97 : 107 - 129
[34] AnFiSA: An open-source computational platform for the analysis of sequencing data for rare genetic disease
Bouzinier, M. A.
Etin, D.
Trifonov, S., I
Evdokimova, V. N.
Ulitin, V
Shen, J.
Kokorev, A.
Ghazani, A. A.
Chekaluk, Y.
Albertyn, Z.
Giersch, A.
Morton, C. C.
Abraamyan, F.
Bendapudi, P. K.
Sunyaev, S.
Krier, B.
JOURNAL OF BIOMEDICAL INFORMATICS, 2022, 133
[35] HydroSignal: open-source internet of things information communication platform for hydrological education and outreach
Kaynak, Baran
Mermer, Omer
Sermet, Yusuf
Demir, Ibrahim
ENVIRONMENTAL MONITORING AND ASSESSMENT, 2025, 197 (04)
[36] Robotics-assisted mass spectrometry assay platform enabled by open-source electronics
Chiu, Shih-Hao
Urban, Pawel L.
BIOSENSORS & BIOELECTRONICS, 2015, 64 : 260 - 268
[37] OpenNAU: An open-source platform for normalizing, analyzing, and visualizing cancer untargeted metabolomics data
Sun, Qingrong
Xu, Qingqing
Wang, Majie
Wang, Yongcheng
Zhang, Dandan
Lai, Maode
CHINESE JOURNAL OF CANCER RESEARCH, 2023, 35 (05) : 550 - +
[38] Towards Certifying the Testing Process of Open-Source Software: New Challenges or Old Methodologies?
Morasca, Sandro
Taibi, Davide
Tosi, Davide
2009 ICSE WORKSHOP ON EMERGING TRENDS IN FREE-LIBRE-OPEN SOURCE SOFTWARE RESEARCH AND DEVELOPMENT, 2009, : 25 - +
[39] Software-Clone Rates in Open-Source Programs Written in C or C plus
Koschke, Rainer
Bazrafshan, Saman
2016 IEEE 23RD INTERNATIONAL CONFERENCE ON SOFTWARE ANALYSIS, EVOLUTION, AND REENGINEERING (SANER), VOL 3, 2016, : 1 - 7
[40] OpenToolFlux: An Open-Source Software for Estimating Gas Fluxes from Automatic Chamber Data
Galea, Carmen
Sanz-Cobena, Alberto
Lassaletta, Luis
Monistrol, Alba
Vallejo, Antonio
Einarsson, Rasmus
AGRONOMY-BASEL, 2023, 13 (11):

← 1 2 3 4 5 →