用 Ada 与 SPARK 加固软件库安全性——以 TCP 协议栈为例
密码学与安全
2021-09-23 v1
摘要
本白皮书展示了如何通过采用 SPARK 技术显著提升一个现有的、用 C 编程语言编写的专业级开源嵌入式 TCP/IP 协议栈实现的保证性、可靠性和安全性。一种多层面方法实现了这一点。首先，TCP 层的 C 代码正被替换为形式化验证的 SPARK（一种受形式化验证工具支持的 Ada 编程语言的子集）。然后，仍用 C 编写且 TCP 层所依赖的底层通过 SPARK 契约建模并使用 KLEE 进行符号执行验证。最后，为调用 TCP 层的上层定义形式化契约。该工作允许检测并修正 TCP 层中的两个缺陷。在一个日益互联、网络安全至关重要的世界中，本工作中详述的强大方法可应用于任何现有的关键 C 库，以显著加固其可靠性和安全性。
引用
@article{arxiv.2109.10347,
title = {Security-Hardening Software Libraries with Ada and SPARK -- A TCP Stack Use Case},
author = {Kyriakos Georgiou and Guillaume Cluzel and Paul Butcher and Yannick Moy},
journal= {arXiv preprint arXiv:2109.10347},
year = {2021}
}
备注
37 pages, 4 figures, 2 tables, white paper, Software/Program Verification