本论文针对 Rust 语言中解析和序列化操作的安全性与性能挑战，提出了一种名为 Vest 的新型框架。Rust 以其内存安全著称，但手写解析器和序列化器仍然容易出错且效率低下。现有方案（如 serde）虽提供自动化，但缺乏形式化验证，且难以应对复杂格式。Vest 结合了形式化验证与高性能实现：首先，用户使用一种安全领域专用语言（DSL）描述数据格式规范；然后，Vest 自动生成经过验证的解析器和序列化器代码。其核心创新在于利用符号执行和 SMT 求解器对生成的代码进行属性验证（如内存安全、无崩溃、格式合规），同时通过编译器优化和运行时技术（如零拷贝、预分配）保持接近手写代码的性能。实验在多个实际数据格式（如 JSON、MessagePack、FlatBuffers）上评估，结果显示 Vest 不仅消除了常见漏洞（如缓冲区溢出、未定义行为），而且性能与 serde 相当或更优，在某些场景下提升高达 30%。该工作为 Rust 生态系统提供了安全与效率兼顾的解析/序列化基础设施，适合编译器工程师、形式化方法研究者及系统程序员阅读。

该论文提出并形式化了一种基于图表解析（chart parsing）的PEG（Parsing Expression Grammar）解析器解释器鲁棒性验证方法。作者定义了一个状态机，该状态机在一个脚手架（scaffold）数据结构上操作，脚手架维护一个状态矩阵，每个条目对应一对位置和非终结符。解析器解释器以惰性方式填充这些条目，记录解析是否成功、失败或陷入循环，从而支持可能左递归的PEG文法并添加循环检测。论文定义了状态上的不变量，并定义了保持这些不变量的解析步进函数。从解析的最终状态可提取独立检查的解析证明表示。作者对一系列演进的PEG形式化定义并证明了图表解析器，并在这些形式化之间进行了大量的证明重用。通过PVS证明系统中的交互与自动化混合，使得证明对特定类型的规范和设计变更具有鲁棒性。论文还讨论了如何主动构建针对解析这类重要问题的鲁棒证明。该工作为解析解释器的正确性提供了形式化保证，对安全领域中的输入验证、反混淆等场景具有理论价值。

本研究报告探讨了字符串逻辑 FC（Function-or-Constraint）在解析器组合中的应用。FC 逻辑最初在数据库理论中用于信息抽取，本文提出其应用范围可以更广，特别是作为统一框架来组合多种解析器，并与语言理论安全（LangSec）原则保持一致。首先，论文回顾了 FC 及其扩展的最新研究文献，并阐述了对于效率的不同评判标准。接着，描述了如何将 FC 及其扩展视为正则表达式的替代品，并在语言理论安全的背景下对其进行定位。最后，利用该模型天然的组合性，将 FC 的多种扩展整合为一个组合解析器的框架。论文的核心贡献在于展示了 FC 逻辑能够统一不同解析器的解析逻辑，减少因解析器互操作产生的安全漏洞，从而提升软件安全性。该工作对于从事形式化方法、解析器设计以及语言理论安全的研究人员和工程师具有参考价值。