卡默勒:OCaml推理验证工具

从社交网络到空间探索 软件是维系世界运行的支柱可我们怎么知道可以信任软件里斯本新科技学院Mário Perera博士及其合作者开发Cameleer软件工具,该软件工具正式验证OCaml写代码,建立数学证明系统按程序员规范工作cameleer是第一个自动推理软件验证工具 程序编译OCaml

世界依赖软件从社会网络等日常任务使用到空间探索等高度关键任务,软件是支撑世界运行的支柱软件开发是一种易出错活动,更不用说它容易恶意攻击偏差软件可产生难为人和代价昂贵的后果2015年,美国7000家Starbucks商店和加拿大1000家Starbucks商店每日系统刷新关闭时发生故障雇员无法接受支付卡或注册更改,因此被迫免费为客户提供咖啡和茶问题几小时后解决 星巴克报告 损失300万到400万元另一实例发生于2008年,当时新Heathrow终端5开机并随机实现现代高效机运系统的承诺系统开机前测试超过12 000件行李并完全工作终端向公众开放时,系统无法处理每天检查的大量行李,发射后仅十天,约42 000袋丢失,500多航班被取消

如何判断软件可信答案之一是软件可靠性测试但这些测试只覆盖软件实际运行中可能执行子集最佳解决办法包括软件开发过程的强健数学保证形式方法是一个计算机科学领域,倡导这种方法,使用严格的数学推理和建模技术描述和认证计算机基础设施部分并提供正式软件验证依据这一做法,里斯本新科技学院的Mário Pereira博士和António Ravara博士及其合作者开发Cameleer工具,这是一个正式OCaml写代码验证软件工具

递减软件验证
演化软件验证包括表达代码正确性并编成一组数学语句,即验证条件并随后证明Pereira解释这包括逻辑规范并附于代码逻辑规范用数学语言写出描述程序执行中某些点必须尊重的属性最后,验证条件生成算法得到实现取代码并配规范并产生验证条件证明这些数学语句正式证明程序执行符合规范中描述的逻辑属性Pereira表示,尽管在过去几十年里推理验证和证明自动化方面有所进步,但功能语言圈通过应用和构件函数构建程序却很少引起注意。

最佳解决办法包括软件开发过程的强健数学保证

OCAML
一种功能语言是OCaml语言,Inria巴黎研究中心开发的工业强度编程语言Ocaml使用软件,如证明助手、自动化求解器和编译器等,由脸书、Bloomberg和Issuu等组织在全世界实施OCaml多范式语言支持功能性、势在必行和面向对象编程模型匹配机制强健灵活模块系统并自动存储管理,以便用于写高效模块化程序,维护类型安全(避免因数据类型差异造成的类型错误)并处理内存变异等副作用

即便这些因素使OCaml代码完全适合正式验证,但OCaml程序很少使用推理验证解释 Pereira此外,Cameleer项目前并不存在可直接处理OCaml编码自动验证工具Ocaml程序设计师选择使用证明自动化时,必须学习鉴别语言,写程序并执行代码提取替代方法使用工具,需要人工验证辅助

Gospel
规格语言是在软件开发期间使用的正式语言,允许在不同层次精确规范需要执行正式软件验证规格语言具体说明软件系统语义和结构,并用于正式验证时提供系统按前规格运行的数学证明

佩雷拉与Arthur Excelaure博士、Jean-Christophe Filliâtre博士和CláudioBeloLourenço博士(Chargueraud等,2019年)一起开发OCAML规范语言-GOSPEL通用Ocam自那以来,GOSPEL发展成成熟项目,目前正在由大型研究集团开发,其中包括ClementPascorto、NicolasOsborne、FrançoisPottier博士和Armaelgueau博士GOSPEL设计方便数据结构与算法验证形式语义定义化为分离逻辑,即程序推理形式GOSPEL提供高层次简明语法,不熟悉分离逻辑程序员可访问GOSPEL开发以具体说明OCaml代码,还打算将其作为通用验证工具,测试特征可应用到其他编程语言

Cameleer为OCaml社区提供强力、可用和多半自动化验证框架

骆驼手
研究者开发Cameleer程序首个自动推理软件验证工具OCamlGOSPEL选择为规范语言,允许向OCaml代码分配可读性强行为规范Cameleer专注于证明自动化并使用GOSPEL附加注释OCaml程序输入将它转换为hisMLwhyML编程和规范语言Whis3平台推算软件验证,特别是自动化证明wh3验证条件生成器生成一套验证条件,发送到执行正式证明的不同求解器

佩雷拉和他的同事选择开发卡美尔验证工具,接受直接以OCaml写成程序输入,而不是专用验证语言表示用户不必完全重写OCaml源码整个验证过程用户只需写OCAML码和GOSPEL规范Cameleer设计为自动生成其他元素后用户不必关注HisML生成程序用户只参与初始描述阶段和进程最后步骤,帮助Wask3关闭证明

Cameleer性能可用性评估 研究人员编译了一组测试案例 由1000多行OCaml代码组成其中包括从现有库实现程序如数值程序、排序和搜索、逻辑算法、数组扫描、高阶实现和数项历史算法这些都是使用Cameleer工具成功验证的Pereira补充道,单靠案例研究集有助于建立全套OCaml代码库

推开软件验证前沿
Pereira描述Cameleer项目研究者如何继续推向软件正式验证前沿开发原理和工具 应用推理验证OCaml写代码至今为止,他们已经开发出强健工具处理OCaml代码并自动验证它是否坚持GOSPEL笔试规范编程程序员使用OCaml-包括非验证专家使用OCaml-关于下一步研究, Pereira表示 : “ 我们的最终目标是生长卡米利尔使用验证工具, 并同时从不同中间验证框架最优特征中受益 。