Cyber Security Daily Radar

#cs.LO

共收录 48 条相关情报。

← 返回所有主题
学术论文2026-10-26 发布INFO

SoK: Timestamps Are Not a Time Model: Rethinking Temporal Reasoning in Host-Based Intrusion Detection

Host-based intrusion detectors order events, window audit streams and sequence attack stages by their timestamps. Every

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.AI#cs.LO
学术论文2026-10-22 发布INFO

FVQKD: A Formal Verification of Quantum Key Distribution Security in Rocq

Quantum key distribution (QKD), whose security is derived from quantum mechanics rather than computational assumptions,

历史摘要 · 未重新核验 · arXiv cs.CR

#quant-ph#cs.LO
学术论文2026-10-20 发布INFO

Proof-Carrying Contracts: Commitments AI Agents Cannot Break

AI agents increasingly act on behalf of people or other agents, purchasing services, exchanging information and delegati

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.AI#cs.LO#cs.MA#eess.SY
学术论文2026-10-20 发布INFO

Local Allow, Global Deny: Why Per-Action Authorization Does Not Compose in LLM Agents

Autonomous LLM agents act through tools under per-action authorization: a local guard screens each tool call in isolatio

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.AI#cs.LO
学术论文2026-10-20 发布INFO

Privacy-Preserving Robustness-Guided Testing

In industries like semi-conductors and aerospace, it is common for the design company to contract out part of the testin

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO
学术论文2026-10-19 发布INFO

Formalization of Rényi Differential Privacy in Isabelle/HOL (Draft version)

Differential privacy (DP) is a gold-standard definition of privacy designed to evaluate the privacy guarantee of databas

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO
学术论文2026-10-07 发布INFO

Hybrid Hierarchical Runtime Verification for Edge-IoT Security: Combining MonPoly and RTLola

Security monitoring of edge-IoT fleets faces three structural challenges. (i) A per-node monitor is cheap but cannot see

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.DC#cs.LO
学术论文2026-10-07 发布INFO

Hierarchical Security Monitoring for Edge-IoT: A Formal Methods Approach

Cyber resiliency in edge-IoT deployments is fundamentally an economic problem: detection must keep critical processes op

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO#cs.SE
学术论文2026-10-06 发布INFO

Multi-Aspect Runtime Verification for Simulation-Based V&V of LLM-Enabled Autonomous Agents

LLM-based agents are entering decision-support roles in defence staff work, where the obligations they must respect are

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.AI#cs.LO
学术论文2026-10-04 发布INFO

StateSync-GKR: Machine-Checking the Trust Chain from Sparse-Merkle State Transitions to GKR Verification

该论文处理的是一个在可验证计算工程中常被忽视的信任缺口：GKR 协议的可靠性界只能保证『关于某个算术电路的输出声明是可信的』，却无法保证『该电路确实编码了应用所期望的状态转移』。作者以稀疏 Merkle 树（SMT）的成员证明、非成员证明与

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO#formal-verification#isabelle-hol#gkr#zero-knowledge#sparse-merkle-tree
学术论文2026-09-30 发布INFO

Security Properties of Neural Networks as Decision Problems

该论文从计算复杂性角度重新审视已部署神经网络的安全认证问题。验证文献长期聚焦鲁棒性等少量性质，但作者指出实际部署中还存在一类未被系统分类的决策问题：模型是否携带训练阶段植入的后门、存储参数故障是否会把网络推入不安全状态、输出是否泄露输入中的

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO#cs.CC#cs.LG#neural-network-verification#computational-complexity#formal-methods
学术论文2026-09-27 发布INFO

Zero-Storage Procedural Neural Synthesis via Boundary Dynamics: Formal Verification in Lean 4 and Bare-Metal Gauntlet Validation

当前主流神经网络推理依赖存放在高带宽显存中的稠密浮点权重矩阵，既受严重的内存墙瓶颈制约，也无法在以太坊虚拟机（EVM）等确定性虚拟机上原生执行。而在 Blum-Shub-Smale 模型下，对连续域上递归动力系统的终止性与算术不变量做验证一

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LG#cs.AI#cs.LO#formal-verification#lean4#neural-inference
学术论文2026-09-22 发布INFO

SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification

该论文聚焦于硬件形式化信息流验证（Information-Flow Verification, IFV）在真实 RTL 上难以扩展的问题。IFV 能为「无秘密依赖的时序与控制行为」提供强保证，但在实际设计中，证明往往因求解器规模爆炸而超时。

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.AR#cs.LO#hardware-security#formal-verification#information-flow#llm
学术论文2026-09-16 发布INFO

Scaling Zero Knowledge UNSAT Verification via Normalized Chaining

该论文关注形式化验证与软件保障中的基础原语——UNSAT 证明（不可满足性证明）。在实际工程中，SAT/SMT 求解器生成的证明往往编码了专有逻辑、内部约束或安全敏感信息，直接公开披露会导致知识产权泄露或攻击面暴露。零知识 UNSAT 认证

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO#zero-knowledge-proof#formal-verification#unsat-proof#privacy-preserving#cryptography
学术论文2026-09-16 发布INFO

CaMeLoT: CaMeL orchestrated with Temporal logic for static verification and liveness

LLM 智能体（agent）会生成并执行多步计划，计划中会调用外部工具；这些工具既可访问私有数据，也可执行命令。在此场景下，安全性并非某个单一步骤的属性，而是由计划所形成的整个执行过程的属性；计划本身就是关键工件，记录了工具调用、控制流与数

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO#agent-security#llm#prompt-injection#formal-verification#model-checking
学术论文2026-09-09 发布INFO

CertiFlash: A Formal Verification Framework for Flash Translation Layers in Computational Solid State Drives

该论文聚焦于以存储为中心的计算（storage-centric computing）场景下固态硬盘（SSD）固件——闪存转换层（FTL）——的安全与正确性问题。研究背景是：数据密集型应用需要把大量数据从存储搬运到计算单元，产生显著的数据移动

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.AR#cs.LO#formal-verification#ssd#flash-translation-layer#storage-security
学术论文2026-09-06 发布INFO

Efficient Hardware Information-Flow Tracking for Pre-Silicon Security Testing

硬件在设计制造之前通常通过寄存器传输级（RTL）仿真进行验证。为了测试与安全相关的信息流属性（如机密性和完整性），可以在设计中自动添加污点逻辑来跟踪信息如何流动。然而，最先进的污点逻辑仪器（如CellIFT）使基于仿真的测试开销过高：在Me

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO#硬件安全#信息流跟踪#RTL#侧信道
学术论文2026-09-03 发布INFO

A Non-Formulable Theorem: A Fundamental Limit of Finite Syntactic Systems and Its Consequences for Security and AI

该论文提出并证明了一个元定理：对于任何一致且具有足够表达能力的有限句法系统S，必然存在至少一个该定理无法自主产生的定理。所谓“有限句法系统”涵盖形式逻辑系统、形式验证器、安全机制、AI系统、法律与经济模型等所有基于有限规则和符号生成机制的体

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.AI#cs.LO#formal-verification#ai-safety#metatheorem
学术论文2026-08-29 发布INFO

Mechanizing Typed Regulatory Actions for Security Tokens: Semantics, Falsification, and Bounded EVM Evidence

该论文针对安全代币（Security Tokens）标准中监管操作语义不明确的问题，提出了一种机械化（machine-checked）的参考执行语义。安全代币标准通常暴露特权转移、冻结、恢复和合规机制，但机制本身并不标识其执行的法律效果或附

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LO#security-tokens#formal-verification#smart-contracts#isabelle
学术论文2026-08-17 发布INFO

Certified but Private: Scalable Zero-Knowledge Proofs for Neural Network Guarantees

本文提出 PANDA，一个基于零知识证明（ZKP）的可扩展系统，用于在保护神经网络模型参数私密性的同时，形式化地证明模型的鲁棒性和公平性。随着机器学习模型在安全关键和法律合规场景中的部署日益增多，模型的鲁棒性和公平性保证变得重要，但模型参数

历史摘要 · 未重新核验 · arXiv cs.CR

#cs.LG#cs.LO#agent-security#llm#zero-knowledge-proof#neural-network