论文标题
验证的Lola规格的生锈监测器
Verified Rust Monitors for Lola Specifications
论文作者
论文摘要
网络物理系统的安全性取决于其监测机制的正确性。如果监视器的规范是手动实现或通过不可靠的软件解释的，则这是有问题的。我们提出了一个验证编译器，该编译器将基于流的监视语言LOLA中给出的规格转换为Rust的实现。生成的代码包含验证注释，使Viper Toolkit能够自动证明功能正确性，没有内存故障和确保终止。根据规范的依赖关系分析，编译器平行于监视器中不同流的评估。我们介绍了通过文献中发现的监视规范获得的令人鼓舞的实验结果。对于每个规范，我们的方法都能够产生正确的证明或发现规范中的错误。
The safety of cyber-physical systems rests on the correctness of their monitoring mechanisms. This is problematic if the specification of the monitor is implemented manually or interpreted by unreliable software. We present a verifying compiler that translates specifications given in the stream-based monitoring language Lola to implementations in Rust. The generated code contains verification annotations that enable the Viper toolkit to automatically prove functional correctness, absence of memory faults, and guaranteed termination. The compiler parallelizes the evaluation of different streams in the monitor based on a dependency analysis of the specification. We present encouraging experimental results obtained with monitor specifications found in the literature. For every specification, our approach was able to either produce a correctness proof or to uncover errors in the specification.
