本文针对现有策略描述语言在表达能力上的不足，提出了一种基于逻辑编程（特别是Datalog）的策略描述语言，旨在支持多层防御（Defense-in-Depth）架构中的细粒度授权。研究背景指出，由于信息系统漏洞难以彻底消除，必须依赖多层防御策略，而每层防御的有效性取决于访问控制的精细程度。现有访问控制模型虽然丰富，但相应的策略语言往往无法准确表达模型的约束条件，尤其是涉及应用程序进程动态状态等复杂决策因素。作者设计的语言允许将多种运行时条件（如进程状态、时间、上下文等）作为决策数据纳入授权规则，从而突破了传统策略语言表达能力的限制。该语言以Datalog实现，利用其逻辑编程特性来支持规则推导与冲突解决。为验证实用性，作者将语言应用于SELinux策略的建模与表达，SELinux是操作系统层面实现多层防御的关键组件。实验从有效性和表达力两个维度进行评估：有效性指语言能否正确表达SELinux原生策略的所有约束；表达力指语言能否以更简洁或更灵活的方式描述相同策略。结果表明，所提语言能够完整覆盖SELinux策略语义，并且在某些场景下提供了更自然的表达能力。本研究的贡献在于：1) 提出了一种形式化且可扩展的策略描述框架，解决了细粒度授权语言的表达缺口；2) 借助Datalog的递归和推理能力，增强了策略的可维护性与自动化分析潜力；3) 通过实际系统（SELinux）的案例证实了方法的可用性。本文适合安全策略研究人员、访问控制模型设计者以及操作系统安全工程师阅读。

本文提出 NeuroLog，一个端到端、无需构建环境的漏洞发现流水线，用于 C/C++ 源代码。核心思路是将 LLM、Datalog（Soufflé）和 SMT 求解器（Z3）分层协作：LLM 逐个函数提取类型化的数据流事实；Soufflé 规则网将这些事实组合成跨函数的发现；Z3 后处理过滤不可行路径并为每个幸存路径输出 SAT 模型。为超越纯静态分析，还引入运行时证据：从少量语料种子导出的可能范围不变量以极低成本收紧 SMT 问题。第二个 LLM 智能体读取每个 SAT 模型并编写 Python 程序生成候选崩溃输入，由 AddressSanitizer 验证。实验覆盖 stb、cJSON、libxml2、FFmpeg demuxer 切片和 curl 8.3.0，重新发现了 8 个 CVE 类问题，包括 CVSS 9.8 的 SOCKS5 堆溢出 CVE-2023-38545。在 libarchive HEAD 上发现 5 个内存安全漏洞（4 个先前未报告），其中 cpio use-after-free 在 7 小时内得到确认。提取阶段约 37 秒、成本 $0.005（stb）；崩溃合成将静态发现转化为 102 字节的 stb_vorbis 崩溃（两轮 LLM 交互）。来自三个 Matroska 种子的似然不变性过滤器消除了 FFmpeg demuxer 可行集中的 13.2%。该方法结合了静态缩小 SMT（Saturn, Pinpoint）和 Datalog 与 SMT（Formulog）的先前工作，新贡献在于 LLM 推导的事实库、无构建流水线以及将 SAT 模型作为合成崩溃输入的制品而非简单的是/否判定。适合安全研究人员、漏洞发现工程师和软件质量保障团队阅读。