MetAcsl：高层属性的规约与验证
软件工程
2019-02-26 v2 密码学与安全
摘要
模块化演绎验证是一种强有力的技术，能够展示程序中每个函数满足其契约。然而，函数契约并未提供关于整个软件模块中哪些高层（例如安全相关）属性实际得以确立的全局视图，使得对这些属性的评估极为困难。为解决此问题，本文提出一种称为元属性（meta-properties）的新规约机制。元属性可视为为一组函数指定的增强型全局不变量，能够表达变量值的谓词，以及内存相关条件（如分离）和读或写访问约束。我们还提出一种自动转换技术，将元属性翻译为常规契约与断言，从而可由传统演绎验证工具证明。该技术已作为名为MetAcsl的Frama-C插件实现，并成功应用于两个示例性案例研究中规约与证明安全和安全相关元属性。
引用
@article{arxiv.1811.10509,
title = {MetAcsl: Specification and Verification of High-Level Properties},
author = {Virgile Robles and Nikolai Kosmatov and Virgile Prevosto and Louis Rilling and Pascale Le Gall},
journal= {arXiv preprint arXiv:1811.10509},
year = {2019}
}
备注
7 pages, slightly extended camera-ready version