A Formally Verified NAT Stack

被引：0

作者：

Pirelli, Solal ^{[1
]}

Zaostrovnykh, Arseniy ^{[1
]}

Candea, George ^{[1
]}

机构：

[1] Ecole Polytech Fed Lausanne, Lausanne, Switzerland

来源：

ACM SIGCOMM COMPUTER COMMUNICATION REVIEW | 2018年 / 48卷 / 05期

关键词：

Network Functions; Software Verification; Kernel Bypass;

D O I：

10.1145/3310165.3310176

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

Prior work proved a stateful NAT network function to be, crash-free, memory safe and semantically correct [29]. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and hardware to be correct. We extend the toolchain to verify the kernel-bypass framework and a NIC driver in the context of the NAT. We uncover bugs in both the framework and the driver. Our code is publicly available [28].

引用

页码：77 / 83

页数：7

共 50 条

[1] A Formally Verified NAT
Zaostrovnykh, Arseniy
Pirelli, Solal
Pedrosa, Luis
Argyraki, Katerina
Candea, George
[J]. SIGCOMM '17: PROCEEDINGS OF THE 2017 CONFERENCE OF THE ACM SPECIAL INTEREST GROUP ON DATA COMMUNICATION, 2017, : 141 - 154
[2] Formally Verified Mathematics
Avigad, Jeremy
Harison, John
[J]. COMMUNICATIONS OF THE ACM, 2014, 57 (04) : 66 - 75
[3] Pragmatics of formally verified yet efficient static analysis, in particular, for formally verified compilers
Monniaux, David
[J]. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2024, 26 (04) : 463 - 477
[4] Formally Verified Montgomery Multiplication
Walther, Christoph
[J]. COMPUTER AIDED VERIFICATION, CAV 2018, PT II, 2018, 10982 : 505 - 522
[5] Formally Verified System Initialisation
Boyton, Andrew
Andronick, June
Bannister, Callum
Fernandez, Matthew
Gao, Xin
Greenaway, David
Klein, Gerwin
Lewis, Corey
Sewell, Thomas
[J]. FORMAL METHODS AND SOFTWARE ENGINEERING, 2013, 8144 : 70 - 85
[6] Formally Verified Superblock Scheduling
Six, Cyril
Gourdin, Leo
Boulme, Sylvain
Monniaux, David
Fasse, Justus
Nardino, Nicolas
[J]. PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22), 2022, : 40 - 54
[7] UTC Time, Formally Verified
de Almeida Borges, Ana
Gonzalez Bedmar, Mireia
Conejero Rodriguez, Juan
Hermo Reyes, Eduardo
Casals Bunuel, Joaquim
Joosten, Joost J.
[J]. PROCEEDINGS OF THE 13TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2024, 2024, : 2 - 13
[8] Formally verified redundancy removal
Hendricx, S
Claesen, L
[J]. DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION 1999, PROCEEDINGS, 1999, : 150 - 155
[9] Plotting in a Formally Verified Way
Melquiond, Guillaume
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (338): : 39 - 45
[10] A formally verified sorting certifier
Bright, JD
Sullivan, GF
Masson, GM
[J]. IEEE TRANSACTIONS ON COMPUTERS, 1997, 46 (12) : 1304 - 1312

← 1 2 3 4 5 →