用智能编程助手修复信息流策略的逻辑框架，提升安全规范精确性
Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI
- 基于认知逻辑构建统一的信息流策略语义框架
- 通过智能助手验证了修正后的形式化，确保逻辑严密性
- 适合安全系统设计者与形式化验证研究者参考
许多高级安全要求涉及程序中信息的允许流动，但因选择性降级问题难以精确表述。认知逻辑的概念已成为政策语义的良好方法，但缺乏稳健的通用框架。2018年CSF会议上发表的一篇题为《假设你知道：关系注释的表达式信息流策略的认知语义》的论文尝试提供统一框架，但其形式化较为粗略，会议期间已宣布需修正。借助代理式AI编程助手，修正后形式化已在Rocq证明助手内完成机器验证。该框架的简洁性与通用性可能有助于比较不同策略描述方式，并利用现有技术实现强制执行。
原文摘要 · Abstract (English)
Many high-level security requirements are about the allowed flow of information in programs and are difficult to make precise because they involve selective downgrading. Notions from epistemic logic have emerged as a good approach to policy semantics but a robust general framework remains elusive. A paper appearing in CSF 2018, entitled ``Assuming You Know: Epistemic Semantics of Relational Annotations for Expressive Flow Policies'', attempted to provide a unifying framework---but the formalization was sketchy and a correction was announced during the conference presentation. With aid from an agentic AI coding assistant, a corrected formalization has been machine checked in the Rocq proof assistant. The simplicity and generality of the framework may help compare different policy specification styles and enforce them by leveraging existing techniques.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。