面向计算机并发程序的形式化验证方法设计

Design of Formal Verification Methods for Computer Concurrent Programs

计算机并发性程序形式化验证一直是软件安全领域的难题。软件并发性漏洞难以被发现,一旦发生问题,会造成不可估量的安全问题。形式化验证基于严格的数学推导基础,采用语言、语义、推理证明三位一体方法,构建形式逻辑系统,以确保被验证系统的安全性能。传统的形式化验证方法由于人工参与多、验证工作量大、验证效率低等不足,难以对计算机并发程序进行严谨高效的模型描述与验证。研究了一种可双向转换的并发性程序形式化验证方法,解决了人工抽象建模存在的工作量大且易出错的问题,并且保证了源码层与抽象层验证的一致性,大幅提升了形式化验证的效率。

Formal verification of concurrent programs is always a difficult problem in the field of software security. Software concurrency vulnerability is difficult to be detected, and once a problem occurs, it will cause immeasurable security incidents. Formal verification is based on a strict mathematical derivation basis. It adopts the trinity method of language, semantics and inference proof to construct a formal logic system to ensure the security performance of the verified system. The traditional formal verification method is difficult to carry out rigorous and efficient model description and verification of computer concurrent programs due to many human participation, large verification workload, and low verification efficiency. A bidirectional conversion concurrent formal verification method is proposed, which solves the problem of manual abstract modeling with heavy workload and prone to errors, and ensures the consistency of source code layer and abstract layer verification and greatly improves the efficiency of formal verification.