A Temporal Logic of Security
提出了一种新的安全策略验证逻辑。该逻辑HyperLTL扩展了线性时间时态逻辑（LTL），并在多个执行路径上使用连接词进行显式和同时量化，从而使HyperLTL能够表达LTL无法表达的信息流安全策略。给出了一个HyperLTL片段的模型检测算法，并在原型模型检测器中实现了该算法。在HyperLTL中可表达的安全策略类的特征在于超属性的算术层次结构。
2013-07-09 cs.CR cs.LO
SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency (Extended version with technical appendices)
我们提出了安全松弛分离逻辑（SecRSL），一个用于证明具有松弛访问的释放-获取片段中的C11程序的信息流安全性的分离逻辑。SecRSL是第一个安全逻辑，它（1）支持对高级语言程序的弱内存推理;（2）继承了分离逻辑的组合，局部推理的优点;（3）表达安全策略，如值依赖分类。据我们所知，SecRSL也是第一个在公理内存模型上开发的安全逻辑。因此，我们也提出了第一个定义的信息流安全的公理弱记忆模型，对我们证明SecRSL声音。SecRSL确保程序满足恒定时间的安全保证，同时没有未定义的行为。我们应用SecRSL来实现和验证一系列并发原语的功能正确性和恒定时间安全性，包括自旋锁模块，混合灵敏度互斥体和多个同步通道实现。后者的经验性能评估表明SecRSL的权力，以支持安全和高性能的并发C程序的开发。
2021-09-09 cs.CR cs.PL
Benchmarking at the Frontier of Hardware Security: Lessons from Logic Locking
集成电路（IC）是所有计算系统的基础。它们包括高价值的硬件知识产权（IP），这些知识产权在通过地理分布的IC供应链时面临盗版、逆向工程和修改的风险。在硬件安全的前沿是各种可信设计技术，这些技术声称可以在设计流程中保护设计免受不可信实体的影响。逻辑锁定是一种保证在IC制造中免受各种威胁的技术。在这项工作中，我们进行了批判性的审查逻辑锁定技术在文献中，并暴露出几个缺点。从其他网络安全比赛中汲取灵感，我们设计了一个社区主导的基准测试活动，以解决评估不足之处。在反思这一过程中，我们揭示了新的光在评估逻辑锁定的不足之处，并揭示了重要的未来方向。所吸取的经验教训可以指导未来在硬件安全的其他领域的努力。
2020-06-11 cs.CR
Towards Tackling Application Logic Flaws through Autonomous Formal-Logic Modeling and Automated Reasoning
Institute of Information Engineering, Chinese Academy of Sciences（中国科学院信息工程研究所）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
本文提出LL-Verifier框架，结合大语言模型自主建模与逻辑模型检查器，自动生成形式逻辑模型并验证，成功在27个物联网访问控制协议中发现多种复杂逻辑漏洞。
2026-10-15 cs.CR
Trace Equivalence and Epistemic Logic to Express Security Properties
在进程代数中，安全属性被表示为进程之间的等价，但哪种等价是合适的并不清楚。这意味着在直观的安全概念和表述之间存在差距。适当的正规化对核查至关重要，我们的目的是弥合这一差距。通过追踪作用域挤出，我们证明了迹等价是全等的。此外，我们构造了一个应用π演算的认知逻辑，并证明了它的逻辑等价性与迹等价性是一致的。我们使用的认知逻辑表明，跟踪等价是相关的存在下，一个非自适应攻击者。
2019-03-09 cs.CR cs.LO
Towards Comprehensively Understanding the Run-time Security of Programmable Logic Controllers: A 3-year Empirical Study
可编程逻辑控制器（PLC）是工业控制系统（ICS）中的核心控制设备，用于控制和监控底层物理设备，如电网。PLC最初被设计为在可信的工业网络中工作，但是一旦部署在面向互联网（或渗透）的网络中，它就可能变得脆弱。然而，缺乏对现代现实世界PLC的运行时间安全性的系统的实证分析。为了缩小这一差距，我们对13家领先供应商的23款现成PLC进行了首次大规模测量。我们发现许多共同的安全问题和未经探讨的影响，在设计和执行时应更认真地加以处理。综上所述，无监督逻辑应用程序可能导致系统资源/权限滥用，这为攻击者提供了远程劫持运行时系统控制流的新手段（而无需利用内存漏洞）; 2）不适当的访问控制机制带来许多未经授权的访问影响; 3）专有或半专有协议在运行时间数据的机密性和完整性保护方面是脆弱的。我们对多个PLC上的相应攻击向量进行了经验评估，这表明安全影响是严重而广泛的。我们的调查结果被报告给相关方负责，并已确认20个错误与7个指定的CVE。
2022-12-29 cs.CR
LpiCT: A logic security analysis framework for protocols
针对pi演算难以及时发现密码协议设计与实现逻辑缺陷的问题，本文融合逻辑规则、二叉树和KMP算法扩展pi演算，提出LpiCT框架，并通过TLS1.3验证其有效性。
2023-11-01 cs.CR cs.LO
A Symbolic Logic with Concrete Bounds for Cryptographic Protocols
本文提出了一种形式逻辑，用于网络协议安全性的定量推理。该系统允许我们导出具体的安全界限，可用于选择密钥长度和其他安全参数。我们提供公理推理数字签名和随机数，安全性的基础上的具体安全的签名方案和伪随机数发生器（PRG）。形式逻辑支持一阶推理和协议不变量推理，并考虑了具体的安全边界。在我们的逻辑中构造的证明也提供了传统的渐近安全保证，因为具体的界限在证明中积累的方式。作为一个说明性的例子，我们使用形式逻辑证明了一个基于签名的挑战-响应协议的认证性质与具体的界限。
2015-11-24 cs.CR cs.LO
SoK: Security of Programmable Logic Controllers
本文对PLC安全进行首次全面知识系统化，梳理17年来攻击与防御研究趋势，提出PLC与ICS威胁分类法并指出可能引发关键基础设施灾难性攻击的研究空白。
2024-03-01 cs.CR
Verification of the IBOS Browser Security Properties in Reachability Logic
本文给出了Illinois浏览器操作系统（IBOS）的重写逻辑规范，定义了可达性逻辑中的同源策略（SOP）等安全属性。它展示了如何使用我们的基于构造器的可达性逻辑定理证明器来演绎验证这些属性。本文还强调了证明中使用的推理技术和三个模块化原则，这些原则对扩大规模和完成验证工作至关重要。
2020-05-25 cs.CR cs.FL cs.LO
A Spatial-Epistemic Logic for Reasoning about Security Protocols
关于安全属性的推理涉及关于系统的信息位于何处以及它如何随时间演变的推理。虽然大多数安全分析技术需要处理信息局部性和知识传播的一些概念，但通常它们不提供用于表达涉及局部知识和知识转移的任意属性的通用语言。在此基础上，我们介绍了一个框架，基于动态空间逻辑规范的安全协议分析。我们的计算模型是现有的π演算的一个变种，而规格表示在一个动态的空间逻辑扩展的认知算子。我们提出的语法和语义的模型和逻辑，并讨论了表达的方法，显示它完成了被动攻击者。我们还证明了通用Dolev-Yao攻击者可以机械地确定任何确定性有限协议，并讨论了如何使用这个结果可能是开放系统的安全属性的原因。我们还提出了一个模型检查算法，我们的逻辑，这已被实现为SLMC系统的扩展。
2011-02-28 cs.CR cs.LO
From Qualitative to Quantitative Proofs of Security Properties Using First-Order Conditional Logic
Cornell University（康奈尔大学）
考虑一阶条件逻辑，其语义由ε-语义的一个变体给出，其中p -> q表示Pr（q| p）超多项式地接近1--比任何逆多项式都快。这种类型的收敛是推理安全协议所必需的。一个完整的公理化提供了这种语义，它示出了如何定性证明的安全协议的正确性可以自动转换为定量证明适合推理有关具体的安全。
2008-04-14 cs.AI cs.CR cs.LO
Design Method for Constant Power Consumption of Differential Logic Circuits
侧信道攻击是灵巧卡和其他嵌入式设备的主要安全问题。他们分析功耗的变化，以找到在安全IC内实现的加密算法的秘密密钥。为了解决这个问题，在安全IC中使用具有独立于输入信号的恒定功耗的逻辑门。本文提出了一种全连接差分下拉网络的设计方法。全连接差分下拉网络是晶体管网络，对于任何互补输入组合，其将网络的所有内部节点连接到网络的外部节点之一。它们是无记忆的，因此具有恒定的负载电容和功耗。这种类型的网络用于专用逻辑门，以保证内部节点对逻辑门总功耗的贡献恒定。
2007-10-25 cs.CR
Epistemic Temporal Logic for Information Flow Security
时间认知逻辑是一个完善的框架，用于表达代理人的知识以及它如何随着时间的推移而演变。在基于语言的安全中，这些是核心问题，例如在解密的情况下。我们建议将这两个领域结合起来。本文提出了一个计算模型和一个认知时态逻辑，用于推理通过观察程序输出获得的知识。这种方法被证明是优雅地捕捉标准的概念，不干扰和解密的文献，以及敏感和公共数据混杂在微妙的方式的信息流属性。
2012-08-30 cs.CR cs.LO cs.MA
Novel Logical Method for Security Analysis of Electronic Payment Protocols
电子支付协议在电子商务安全中起着至关重要的作用，是电子商务活动安全运行的基础。形式化方法是验证协议安全性的有效方法。但目前的形式化方法缺乏对电子支付协议中时效性的描述和分析。为了提高电子支付协议的分析能力，提出了一种分析电子支付协议中可追究性、公平性和及时性等安全属性的新方法。该方法扩展了已有的逻辑方法，增加了简洁的时间表示和分析方法.它能够描述事件的时间，扩展了逻辑推理规则的时间特性。利用该方法对Netbill协议进行了分析，发现由于时间性问题，该协议的公平性不理想。结果表明，新方法能够分析电子支付协议的关键属性。此外，该方法还可用于分析密码协议的其他时间特性。
2017-06-30 cs.CR cs.LO
JEV as a Judge for Agent Trace Security: An Empirical Comparison with Generative LLM Judges
针对生成式大模型评判智能体安全存在延迟高、输出易失效的问题，该研究提出用类型化决策模型JEV做回溯轨迹分类，实验证明其在多基准上整体F1更高、成本更低，可作为经济型安全筛选方案。
2026-09-28 cs.CR
Security Policies for WFMS with Rich Business Logic - A Model Suitable for Analysis
本文介绍了一个正式的元模型规范的安全策略的工作流在网上服务系统的设计是适合建模和分析复杂的业务相关的规则，以及传统的访问控制。一个翻译的模型到一个有色Petri网和一个例子的网上银行系统的政策。通过编写用于查询Petri网的结果状态空间的谓词，可以在形式化模型和安全策略的更高级别描述之间建立连接，从而表明用于验证这些描述的预期方法的可行性。由于与不同业务服务相关的任务之间的独立性，由元模型内的信息流中的限制表示，状态空间可以被分割以进行分析，从而避免状态空间爆炸问题。相关的现有模型进行了讨论，指出在业务规则的表达性和不安全的状态路径，而不是简单的不安全状态的分析，在建议的模型中的增益。成功的代表性和分析的政策，从例子结合推理的一般情况下证明了所提出的方法，其预期的应用程序的充分性。
2013-04-22 cs.CR
SoK: Attacks on Industrial Control Logic and Formal Verification-Based Defenses
可编程逻辑控制器（PLC）在工业控制系统中起着至关重要的作用。PLC程序中的漏洞可能导致攻击，对关键基础设施造成毁灭性后果，如Stuxnet和类似攻击所示。近年来，我们看到PLC控制逻辑报告的漏洞呈指数级增长。回顾过去的研究，我们发现广泛的研究探讨了控制逻辑修改攻击，以及基于形式化验证的安全解决方案。我们对这些研究进行了系统化，并发现了可能危及整个控制链并逃避检测的攻击。然而，大多数的形式化验证的研究调查的ad-hoc针对PLC程序的技术。我们发现了形式化验证的各个方面的挑战，这些挑战来自于（1）不断扩展的攻击面，（2）程序执行期间的实时约束，以及（3）给定对不同技术的专有和特定于供应商的依赖性的安全评估中的障碍。在知识系统化的基础上，我们为未来的研究方向提供了一套建议，并强调了除了安全问题之外，还需要防御安全问题。
2021-03-23 cs.CR
Hardware Security Evaluation of MAX 10 FPGA
随着物联网设备的普及，对数据的机密性和完整性的需求越来越大。基于可重构逻辑（CPLD或FPGA）的解决方案比ASIC和MCU/SoC替代方案具有一定的优势。可编程逻辑器件是保密性和可编程性的理想选择。在这种情况下，CPLD/FPGA器件的硬件安全性至关重要。本文展示了英特尔MAX 10设备的硬件安全性的初步评估。这些FPGA是要求广泛功能和高安全性的应用程序的最合适的候选人之一。揭示了它们的强大和薄弱的安全方面，并提出了一些建议，以应对实际设计中可能存在的安全漏洞。这是一份可行性研究报告。其目的是突出最容易受到数据提取和逆向工程攻击的区域。这样就可以对具体的关切领域进行进一步调查。
2019-10-11 cs.CR
Modeling Adversaries in a Logic for Security Protocol Analysis
安全协议分析的逻辑需要形式化的对手模型，指定对手的能力。一个常见的模型是Dolev-Yao模型，它只考虑能够编写和重放消息并使用已知密钥解密的对手。Dolev-Yao模型是一个有用的抽象，但它有一些缺点：它不能处理知道协议特定信息的对手，也不能处理概率概念，例如对手试图猜测密钥。我们展示了如何使用一个逻辑与算法知识的概念，我们可以分析不同的对手模型下的安全协议。粗略地说，假设对手使用算法来计算他们的知识;对手的能力是通过对所使用的算法进行适当的限制来捕获的。我们展示了如何在这种情况下对标准的Dolev-Yao对手进行建模，以及如何捕获更一般的能力，包括特定于协议的知识和猜测。
2012-03-09 cs.CR cs.LO
Antaeus: Hunting Repository-Level Logic Vulnerabilities via Context-Grounded LLM Reasoning
University College London（伦敦大学学院）；University of Bologna（博洛尼亚大学）
提出Antaeus框架，通过仓库级代码上下文锚定LLM推理，结合函数优先级排序、上下文推理、比较验证和结构化报告，有效检测逻辑漏洞，在28个仓库中检测出15个漏洞，优于基线方法。
2026-09-02 cs.CR
Formally Proved Security of Assembly Code Against Power Analysis: A Case Study on Balanced Logic
在他在CHES 2004的主题演讲中，Kocher主张侧信道攻击是一个例子，说明正式的密码学并不像人们认为的那样安全，因为一些假设（例如，在计算期间没有辅助信息可用）没有被建模。这种失败是由形式化方法关注模型而不是实现造成的。在本文中，我们提出了形式化的方法和工具，设计保护代码，并证明其安全性的权力分析。这些正式的方法避免了模型和实现之间的差异，工作在后者，而不是一个高层次的模型。事实上，我们的方法允许我们（a）自动插入一个功率平衡对策直接在汇编级，并证明诱导的代码转换的正确性;和（b）证明所获得的代码是平衡的一个合理的泄漏模型。我们还展示了如何描述硬件的特征，以使用最大化模型相关性的资源。实现我们的方法的工具，然后证明在一个案例研究中的8位AVR单片机，我们产生了一个可证明的保护目前的实施，揭示了至少250倍以上的抵抗CPA攻击。
2015-06-17 cs.CR
Logic layer Prompt Control Injection (LPCI): A Novel Security Vulnerability Class in Agentic Systems
Qorvex Consulting（Qorvex咨询公司）；Roshan Consulting（Roshan咨询公司）；OWASP Top 10 for LLMs（OWASP顶级LLM列表）；NIST GenAI PWG（NIST生成AI工作组）；Deloitte Enterprise Risk | Internal Audit | Technology GRC（德勤企业风险管理|内部审计|技术治理与合规）；Reykjavik University（雷克雅未克大学）；Nokia, Technology Center, Ulm, Germany（诺基亚技术中心，德国乌尔姆）
本文提出逻辑层提示控制注入（LPCI），一种针对智能体系统的新型安全漏洞，通过记忆或工具输出嵌入隐蔽载荷，绕过过滤器并跨会话触发未授权行为。
2025-08-06 cs.AI cs.CR cs.LG
LogiC-Diff: Embedding Security Properties Into AI-Enabled Cyber-Physical Systems
Vanderbilt University（范德堡大学）；University of Virginia（弗吉尼亚大学）
提出逻辑条件双阶段扩散框架，将STL规范嵌入CPS预测，同时修复输入与细化输出，提升对抗鲁棒性和规范符合性。
2026-10-01 cs.AI cs.CR
Security Properties through the Lens of Modal Logic
本文提出基于模态逻辑的安全属性推理框架，可统一刻画保密性、完整性、鲁棒去分类和透明背书等多种进展及终止敏感变体，揭示标准定义中的隐藏假设并支持未来扩展。
2023-09-18 cs.CR cs.LO cs.MA
Distillability of LLM Security Logic: Predicting Attack Success Rate of Outline Filling Attack via Ranking Regression
本文通过排序回归方法，研究LLM安全逻辑的可蒸馏性，提出改进的轮廓填充攻击以预测攻击成功率，实验表明代理模型在预测安全边界方面具有较高准确性。
2025-11-27 cs.AI cs.CR
POR for Security Protocol Equivalences: Beyond Action-Determinism
形式化方法已被证明是自动分析协议的有效方法。在过去的几年里，许多研究都集中在验证协议上的迹等价性，这主要用于对许多有趣的隐私属性进行建模，例如，匿名或不可链接。许多用于检查跟踪等价性的工具依赖于对并发操作的所有交织的幼稚且昂贵的探索，这需要偏序约简（POR）技术。在本文中，我们提出了第一个POR技术协议的等价性，不依赖于一个动作确定性的假设：我们重铸的跟踪等价性问题作为一个可达性问题，持久性和睡眠集技术可以应用，我们展示了如何有效地应用这些结果的上下文中的符号执行。我们报告的原型实现，改进工具DeepSec。
2018-04-24 cs.CR
The First-Order Logic of Hyperproperties
我们研究了超性质的逻辑基础。超属性将迹属性（迹的集合）推广到迹的集合的集合。超性质最突出的应用是信息流安全：信息流策略通过比较两个或多个执行轨迹来表征系统的秘密性和完整性，例如通过比较外部观察者对由秘密变量的不同值产生的执行轨迹的观察。本文建立了超性质时态逻辑与一阶逻辑之间的第一个联系。坎普的开创性定理（在制定由于Gabbay等人）指出线性时间时态逻辑（LTL）在表达上等价于有序自然数上的一阶逻辑。我们介绍了一阶逻辑的轨迹集，并证明了HyperLTL，LTL的超性质的扩展，是严格包含在这个逻辑。此外，我们展示了一个片段，是表达等价于HyperLTL，从而建立坎普的超性质定理。
2017-01-09 cs.CR cs.LO math.LO
Security Issues on the OpenPLC project and corresponding solutions
针对OpenPLC缺乏安全防护的问题，本文通过威胁建模、漏洞分析与实验实施控制逻辑注入攻击，并提出安全增强版本OpenPLC Aqua。
2025-09-03 cs.CR
Security Analysis for SCONE Logic Locking
New York University Abu Dhabi（阿布扎比纽约大学）；New York University Tandon School of Engineering（纽约大学坦登工程学院）
研究SCONE逻辑锁定的两种实现的安全性，对无ES变体证明其扩展接口未增加有效暴力破解维度，对有ES变体提出多项式时间白盒攻击等，还提出轻量级非线性缓解方法。
2026-07-07 cs.CR
ANCHOR: logically-centralized security for Software-Defined Networks
虽然SDN的集中化带来了更快的创新速度等优势，但它也破坏了传统架构对不同威胁的一些自然防御。关于SDN的文献大多关注功能方面，尽管有一些关于非功能属性（如“安全性”或“可靠性”）的具体工作。虽然以临时、零敲碎打的方式处理后者可能会奏效，但这很可能导致效率和效力问题。我们认为，作为SDN鲁棒性的支柱，非功能属性的实施需要一种系统性的方法。作为一个一般的概念，我们提出了锚，一个子系统架构，促进非功能属性的逻辑集中。为了证明这一概念的有效性，我们在本文中重点关注“安全性”：我们确定了SDN中当前的安全漏洞，并以全局和一致的方式使用适当的安全机制填充架构中间件。锚点提供的基本安全机制包括可靠的熵和弹性伪随机生成器，以及用于SDN设备的安全注册和关联的协议。我们在论文中声称并证明，集中这些机制是其有效性的关键，允许我们：为这些属性定义和执行全局策略;降低控制器和转发设备的复杂性;确保关键服务的更高水平的鲁棒性;促进非功能性属性执行机制的互操作性;并促进架构本身的安全性和弹性。我们讨论的设计和实现方面，我们证明和评估我们的算法和机制，包括形式化的主要协议和验证其核心的安全属性使用的Tamarin证明。
2018-12-31 cs.CR cs.NI
Automated Hardware Logic Obfuscation Framework Using GPT
本研究提出名为Obfus-chat的新型框架，利用GPT模型自动化硬件逻辑混淆流程，经基准测试与攻击验证，其在保障硬件IP安全上兼具效力与效率。
2024-05-20 cs.CR
Partial Order Reduction for Security Protocols
安全协议是使用密码学进行通信的并发进程，目的是实现各种安全属性。最近关于它们的形式化验证的工作带来了用于决定迹等同性的过程和工具（例如，匿名性、不可链接性、投票保密性）。然而，这些程序是基于一个天真的符号探索所考虑的过程中，毫不奇怪，大大限制了验证工具的可扩展性和实际影响的所有痕迹。在本文中，我们克服了这个困难，通过发展偏序约简技术的安全协议的验证。我们提供了减少的过渡系统，最佳地消除冗余的痕迹，这是足够的模型检查跟踪等价性的协议通过符号执行。我们已经在工具Apte中实现了我们的减少，并证明了它在各种协议上实现了预期的加速。
2015-09-07 cs.CR cs.LO
ATM: a Logic for Quantitative Security Properties on Attack Trees
针对攻击树缺乏易懂且强大的定量属性查询工具的问题，本文提出ATM逻辑，支持成本、概率等安全属性规范与假设场景构建，结合二元决策图实现属性检查与指标计算，并通过CubeSAT案例验证了其潜力。
2024-05-17 cs.CR cs.LO
Instrumenting Transaction Trace Properties in Smart Contracts: Extending the EVM for Real-Time Security
针对智能合约无法实时读取交易迹以阻止只读重入等攻击且现有安全属性gas消耗高的问题，提出修改EVM和以太坊客户端，使合约能实时验证交易迹属性，并使用PLTL形式化这些属性，显著增强安全性。
2024-08-26 cs.CR cs.LO
Evaluating the Indistinguishability of Logic Locking using K-Cut Enumeration and Boolean Matching
Sandia National Laboratories（桑迪亚国家实验室）
本文提出基于k-割分布比较的新方法，评估逻辑锁的不可区分性，结果显示其在存在重合成时仍能保持较高准确性，表明现有锁机制缺乏不可区分性保障。
2026-02-24 cs.CR
Is Robust Design-for-Security Robust Enough? Attack on Locked Circuits with Restricted Scan Chain Access
逻辑锁的安全性受到各种攻击的质疑，特别是基于布尔可满足性（SAT）的攻击，该攻击利用工作芯片中的扫描访问。在其他技术中，提出了鲁棒的安全设计（DFS）架构以限制任何未经授权的扫描访问，从而挫败SAT攻击（或依赖于扫描访问的任何其他攻击）。然而，在这项工作中，我们成功地打破了这种技术，恢复秘密密钥，尽管缺乏扫描访问。我们的安全性分析的几个基准电路保护的强大的DFS架构证明了我们的攻击的有效性，平均~95%的关键位被正确地恢复，在大多数情况下几乎100%。为了克服这一点和其他流行的攻击，我们提出了一种防御，从根本上改变了强大的DFS技术，新的防御可以承受所有的逻辑锁定攻击。我们观察到，平均而言，比健壮DFS设计（~5.15%）更低的面积开销（~1.65%），以及类似的测试覆盖率（~99.88%）。
2019-06-18 cs.CR
GID: Graph-based Intrusion Detection on Massive Process Traces for Enterprise Security Systems
入侵检测系统是企业安全体系结构的重要组成部分。特别是，基于异常的入侵检测系统已被广泛应用于检测偏离大多数的异常进程行为。然而，这种异常行为通常由一系列低级别的异质事件组成。低级别事件和高级别异常行为之间的间隙使得很难推断哪些单个事件与真正的异常活动相关，特别是考虑到其间发生了大量“嘈杂”的低级别事件。因此，集中于检测单个实体/事件的现有工作难以实现高检测精度。与以往的工作不同，我们设计并实现了GID，一个有效的基于图的入侵检测技术，可以识别异常事件序列，从一个巨大的异构进程跟踪高准确率。GID首先构建一个紧凑的图结构来捕获不同系统实体之间的交互。然后利用随机游走技术对所构造的无环有向图进行过程路径可疑度或异常度的度量。为了消除路径长度对异常评分的影响，引入Box-Cox幂变换对异常评分进行归一化，使不同长度路径的异常评分分布一致.该优化方案进一步提高了可疑路径发现的效率。我们完全实现了我们的GID算法，并将其部署到实际的企业安全系统中，它极大地帮助检测高级威胁，并优化事件响应。在系统监控数据集上执行GID，显示GID高效（每分钟约200万条记录）和准确（检测率高于80%）。
2016-08-08 cs.CR
Detecting Logic Vulnerabilities Across the Contract and Device Layers of Blockchain-Enabled IoT With Multi-Agent Heterogeneous Graph Attention
Faculty of Data Science, City University of Macau（澳门城市大学数据科学学院）；Guangzhou University（广州大学）
针对区块链物联网中合约与设备层逻辑漏洞，提出多智能体异构图注意力框架MA-HGAT，统一建模多类工件，支持多种检测任务并实现轻量级边缘部署。
2026-09-17 cs.CR
Formal Verification of Probing Security via Conditional Independence
Faculty of Education and Integrated Arts and Sciences Waseda University（早稻田大学教育综合科学部）
提出基于概率分离逻辑的方法，通过连接非干扰性与条件独立性，利用Lilac分离逻辑验证掩码算法的探测安全性，并提供证明规则。
2026-05-25 cs.CR cs.LO
Exploiting the Lock: Leveraging MiG-V's Logic Locking for Secret-Data Extraction
该研究针对商用逻辑锁定 RISC-V 处理器 MiG-V，在运行 SSL 算法时篡改逻辑锁定密钥，发现单比特变化即可泄露全部加密密钥。
2024-08-09 cs.AR cs.CR
Usability Study of Security Features in Programmable Logic Controllers
University of Bristol（布里斯托大学）
本文通过研究发现PLC安全配置的可用性问题，揭示了误配置原因，并提出设计建议以提升工业安全的可用性。
2026-02-24 cs.CL cs.CR cs.HC
GNN-Based Code Annotation Logic for Establishing Security Boundaries in C Code
University of Würzburg（维尔茨堡大学）；Huawei Technologies（华为技术有限公司）
本文提出代码标注逻辑CAL，利用图神经网络自动识别C代码中需隔离到可信执行环境的安全敏感组件，以优化可信计算基并减少攻击向量。
2024-11-19 cs.CR cs.LG
RESAA: A Removal and Structural Analysis Attack Against Compound Logic Locking
本文提出了RESAA框架，通过分类CLL锁定设计、识别关键逻辑门并执行攻击来揭示密钥，实验证明其在无预言机模型下准确率达92.6%，揭示了复合逻辑锁定的安全漏洞。
2024-09-25 cs.CR
TraceLLM: Security Diagnosis Through Traces and Smart Contracts in Ethereum
针对以太坊智能合约安全分析存在的代码未验证、轨迹分析依赖人工等问题，提出结合执行轨迹与反编译代码的TraceLLM框架，构建首个相关基准，在多组实验中准确率优于基线，泛化性较强。
2025-09-03 cs.CR cs.ET cs.SE
Toward Trusted Sharing of Network Packet Traces Using Anonymization: Single-Field Privacy/Analysis Tradeoffs
分布式安全分析需要共享网络数据。为了共享而对网络数据进行分析，在隐私保护与安全分析能力之间建立了基本的权衡。这种隐私/分析权衡已经被许多研究人员所承认，但这是第一篇提供实证测量来表征企业数据集的隐私/分析权衡的论文。具体来说，我们在网络数据包跟踪中的单个字段上执行匿名化选项，然后使用入侵检测系统警报作为安全分析功能的代理进行测量。我们的结果显示：（1）两个字段具有零和折衷（更多的隐私减少安全分析，反之亦然），以及（2）八个字段具有更复杂的折衷（不是零和），其中隐私和分析两者都可以同时完成。
2007-10-26 cs.CR cs.NI
Challenging the Security of Logic Locking Schemes in the Era of Deep Learning: A Neuroevolutionary Approach
RWTH Aachen University（亚琛工业大学）
逻辑锁定是在整个集成电路设计和制造流程中保护硬件设计完整性的重要技术。然而，近年来，各种去混淆攻击的引入彻底挑战了锁定方案的安全性。与大多数研究分支一样，深度学习也被引入逻辑锁定领域。因此，在本文中，我们提出了快照：一种新的攻击逻辑锁定，是第一种利用人工神经网络直接预测一个关键位值从锁定合成门级网表，而不使用黄金参考。因此，与现有工作相比，该攻击使用了更简单但更灵活的学习模型。两种不同的方法进行评估。第一种方法是基于一个简单的前馈全连接神经网络。第二种方法利用遗传算法来进化更复杂的专门用于给定任务的卷积神经网络架构。攻击流程提供了一个通用的和可定制的框架，用于使用机器学习技术攻击锁定方案。我们针对两种实际攻击场景对SnapShot进行了广泛的评估，包括参考基准电路以及经过硅验证的RISC-V核心模块。评估结果表明，SnapShot在选定的攻击场景中实现了82.60%的平均关键预测准确率，与最先进的技术相比，性能显著提高了10.49个百分点。此外，SnapShot在所有评估基准上都优于现有技术。结果表明，常见的逻辑锁方案的安全基础是建立在可疑的假设。评估的结论提供了对设计未来逻辑锁定方案的挑战的见解，这些方案能够抵御机器学习攻击。
2020-11-30 cs.CR cs.LG cs.NE
Verifying Security Policies in Multi-agent Workflows with Loops
我们认为基于Web的工作流，如会议提交系统，如EasyChair的信息流安全策略的自动验证。我们的工作流描述语言允许循环，非确定性的选择，和无限数量的参与代理。信息流策略在超属性的时态逻辑中指定。我们证明了验证问题可以归结为一阶线性时间时序逻辑公式的可满足性，并为相关类别的工作流和规范提供可判定性结果。我们报告的一系列基准上实现我们的方法所获得的实验结果。
2017-08-29 cs.CR cs.LO
Toward Efficient Evaluation of Logic Encryption Schemes: Models and Metrics
过去十年对逻辑加密的研究产生了各种技术来防止不同的安全威胁，例如特洛伊木马插入、知识产权泄露和逆向工程。然而，在一组统一的度量和模型上几乎没有达成一致，以有效地评估所达到的安全级别以及安全性和开销之间的权衡。本文解决了上述挑战，依赖于一个通用的逻辑加密模型，可以包括所有现有的技术，和一组统一的指标，可以捕获多个，可能相互冲突的安全问题。我们将我们的建模方法应用于四种最先进的加密技术，表明它可以快速准确地评估设计权衡，平均预测误差至少比以前的方法小2倍，以及复合加密方法的评估。
2020-07-29 cs.CR cs.SY eess.SY
System M: A Program Logic for Code Sandboxing and Identification
执行不受信任代码的安全敏感应用程序通常通过将代码的语法与已知的正确值进行比较来检查代码的完整性，或者对代码进行沙箱化以包含其影响。系统M是一种新的程序逻辑，用于推理这种安全敏感的应用程序。系统M扩展了Hoare类型论（HTT）来追踪安全属性，并包含两个新的推理原则。首先，它的类型系统将逻辑相等内在化，便于对检查代码完整性的应用程序进行推理。第二，限制规则仅基于计算的沙箱的知识将效应类型分配给计算。我们证明了系统M相对于一个步骤索引的基于跟踪的语义模型的可靠性。我们说明了这两个新的推理原则的系统M通过验证Memoir，以前提出的可信计算系统，以确保状态的连续性隔离的安全敏感的应用程序的设计的主要完整性属性。
2015-01-22 cs.CR cs.LO cs.PL
Efficient Hardware Information-Flow Tracking for Pre-Silicon Security Testing
Princeton University（普林斯顿大学）；MIT CSAIL（麻省理工学院计算机科学与人工智能实验室）；EPFL（洛桑联邦理工学院）
针对RTL仿真中污点逻辑开销过大的问题，提出CEGAR-T框架，自动合成最小化插桩开销且无误报的污点逻辑，在RISC-V核上大幅降低插桩和仿真开销。
2026-09-09 cs.CR cs.LO
Knowledge and Security
认知概念，在某些情况下，认知逻辑，已被用于安全研究，以形式化系统的安全属性。本调查说明了其中的一些用途，重点是在密码协议的背景下，并在多级安全系统的背景下的机密性。
2013-05-04 cs.CR cs.LO
Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic
Surrey Centre（萨里中心）；IMSc Chennai（印度数学科学研究所钦奈分所）；Azim Premji University（阿齐姆·普雷吉大学）；University of Surrey（萨里大学）
该研究提出理性Dolev--Yao攻击者模型，用加权交替时间时序逻辑验证协议理性安全性，证明其可判定性与复杂性，并通过认证支付和ThreeBallot案例展示其应用。
2026-08-25 cs.CR cs.GT
Temporal Attack Pattern Detection in Multi-Agent AI Workflows: An Open Framework for Training Trace-Based Security Models
SAP；OWASP Gen AI Security Project（OWASP生成人工智能安全项目）；Agentic Security Initiative (ASI)（代理安全倡议（ASI））
本文提出了一种开放框架，通过合成轨迹生成和微调语言模型，提升多智能体AI工作流中时间攻击模式检测的准确性，并公开了相关数据集和评估基准。
2025-12-29 cs.AI cs.CR
