Automated Abstraction Refinement for Information Flow Security in Embedded Systems
本文聚焦安全敏感嵌入式系统的信息流安全验证问题。信息流分析（IFA）是验证机密性与完整性的重要手段，但嵌入式系统天然具有并发性与时间相关性，导致既有 IFA 方法往往陷入两难：要么抽象过于粗糙而精度不足、无法判定非法信息流是否存在，要么保持
#information-flow
共收录 14 条相关情报。
← 返回所有主题SLED-IFV: Solver-Validated LLM-Guided Decomposition for Scalable Hardware Information-Flow Verification
该论文聚焦于硬件形式化信息流验证（Information-Flow Verification, IFV）在真实 RTL 上难以扩展的问题。IFV 能为「无秘密依赖的时序与控制行为」提供强保证，但在实际设计中，证明往往因求解器规模爆炸而超时。
POLYFLOW: A Neuro-Symbolic Framework for Static Cross-Language Information Flow Analysis
现代软件系统通常由多种编程语言混合构建（如 Python 与 C、Java 与 C 的交互），这种跨语言架构会因语言间的语义差异和隐式交互引入难以察觉的漏洞。传统静态分析器受限于不同语言语义的异构性，往往无法有效建模跨语言的数据流；动态分析
Sound Enforcement of Dynamic Release Information Flow Policy-Full Version
本文研究信息流分析（Information Flow Analysis）在真实系统中的应用问题。信息流分析是评估机密性和完整性的主要方法，但实际采用率不高，根本原因在于理论与实践的差距：现有技术通常假设安全策略是静态的（即数据保密性不变），
Renaming or Tightness: Enforcing Disjunctive Information Flow Policies
本文研究分离式信息流策略的强制执行问题。分离式策略允许一个值最多依赖于两个秘密之一，而不能同时依赖于两者，例如分析师只能查阅一个客户的文件而不能同时查阅两个，或者分割的秘密只能释放其中一部分。这类策略不满足格结构，Hunt和Sands提出使
Assuming You Knew: Fixing an Epistemic Semantics for Flow Policies Using Agentic AI
该论文针对程序信息流策略的语义形式化问题进行修正与验证。许多高级安全需求涉及程序中允许的信息流动，但由于存在选择性降级（selective downgrading）而难以精确表达。认识逻辑（epistemic logic）中的概念被视为一种
Checking Information Flow in Cloud-based IoT Access Control Policies (Extended Version)
本文研究云环境下物联网（IoT）访问控制策略中的信息流安全问题。许多云服务商（如AWS IoT Core）提供访问控制机制，但其配置不当可能导致严重安全漏洞。作者指出，在设备具有不同信任级别或隶属于不同子系统的场景中，仅独立验证单个权限是否
The Duality of Information Flow: Reconciling Robust Downgrading with Non-Interference
该论文探讨了程序安全中非干扰属性（non-interference）与信息降级（downgrading）之间的经典矛盾。非干扰是机密性和完整性的最高安全保证，但严格的非干扰会阻止大多数实际程序完成其功能，因为它们需要泄露或修改信息。传统方法
Type-based information flow analysis for $π$-calculus with a dynamically extensible security lattice
本文提出了一种基于类型系统的安全信息流分析方法，用于处理动态可扩展安全格（security lattice）。该方法扩展了Kobayashi基于类型的π-演算安全信息流分析，π-演算是一种支持顺序和并发计算的表达性模型，具有简洁的语法、基于
Information flow security on persistent memory
该论文针对持久内存（Persistent Memory）这一新兴内存范式中的信息流安全（information flow security）问题展开研究。持久内存能够提升运行时效率并支持程序在断电或系统崩溃后恢复，但现有研究多聚焦于功能正确
Guarded Equivalence Predicates for Scalable Formal Hardware Information-Flow Verification
本文针对硬件信息流（information-flow）的形式化验证中可扩展性不足的问题，提出了一种名为“受保护等价谓词”（Guarded Equivalence Predicates）的方法。在硬件安全验证中，自组合（self-compos
Beyond Epsilon: A Principled QIF Framework for Local Differential Privacy
本文针对本地差分隐私（LDP）协议缺乏系统化比较方法的问题，提出了基于定量信息流（QIF）的分析框架。当前LDP领域通常使用隐私预算ε作为隐私度量，但ε仅能约束最坏情况下的区分性；其他比较则依赖效用驱动分析，即针对给定隐私预算ε评估机制保留
Language-Based Agent Control
本文提出了一种名为“基于语言的智能体控制”（LBAC）的新型编程模型，旨在解决智能体应用中的安全控制问题。传统的编程语言中，静态类型和运行时强制执行已被用于确保程序满足用户指定的策略（如访问控制、信息流、数据来源等）。LBAC的核心思想是将
Mechanized Type Safety for Gradual Information Flow.
本文研究了如何在证明助手中对一种具有渐进信息流标签的安全类型语言进行形式化建模。渐进信息流标签允许在类型系统中动态调整安全级别，从而在编译时静态检查和运行时动态检查之间取得平衡。作者首先给出了该语言的定义解释器语义，并在证明助手中实现，然后