Type-Directed, Secure-by-Construction Enclave Partitioning for LLVM
本文针对可信执行环境（TEE）与低层语言（如 LLVM IR）结合时面临的安全分区问题展开研究。TEE 通过 enclave 提供硬件级隔离，但仅依靠它无法保证信息流安全；LLVM 这类语言允许不受限制的指针操作和非结构化控制流，进一步加剧
#type-system
共收录 8 条相关情报。
← 返回所有主题Sound Enforcement of Dynamic Release Information Flow Policy-Full Version
本文研究信息流分析（Information Flow Analysis）在真实系统中的应用问题。信息流分析是评估机密性和完整性的主要方法，但实际采用率不高，根本原因在于理论与实践的差距：现有技术通常假设安全策略是静态的（即数据保密性不变），
Renaming or Tightness: Enforcing Disjunctive Information Flow Policies
本文研究分离式信息流策略的强制执行问题。分离式策略允许一个值最多依赖于两个秘密之一，而不能同时依赖于两者，例如分析师只能查阅一个客户的文件而不能同时查阅两个，或者分割的秘密只能释放其中一部分。这类策略不满足格结构，Hunt和Sands提出使
Type-based information flow analysis for $π$-calculus with a dynamically extensible security lattice
本文提出了一种基于类型系统的安全信息流分析方法，用于处理动态可扩展安全格（security lattice）。该方法扩展了Kobayashi基于类型的π-演算安全信息流分析，π-演算是一种支持顺序和并发计算的表达性模型，具有简洁的语法、基于
Owl: Compositional Verification of Security Protocols via an Information-Flow Type System.
该论文提出了一种名为Owl的新框架，用于安全协议的组合验证。现有的计算安全协议验证工具要么缺乏模块化，要么缺乏自动化。Owl通过新颖地使用信息流类型和细化类型来实现加密安全的证明。该框架允许对安全协议进行基于类型的模块化描述，其中不相交的子
Extract: A PHP Foot-Gun Case Study.
该论文以PHP语言中的类型体系为研究对象，通过挖掘特定API（如extract函数）的潜在陷阱，系统分析了PHP类型系统在使用类似extract这类函数时可能引发的安全漏洞。作者通过构造一系列案例，展示了攻击者如何利用类型混淆与变量覆盖机制
Vulnerability Flow Type Systems.
本文提出了一种基于类型系统的方法来推导程序暴露的抽象“怪异机器”（weird machines）。背景是：广泛使用的关键软件系统中存在潜伏漏洞，攻击者可触发并级联这些漏洞，使程序行为异常，形成可被利用的编程模型。作者创新性地设计了一种信息流
Language-Based Agent Control
本文提出了一种名为“基于语言的智能体控制”（LBAC）的新型编程模型，旨在解决智能体应用中的安全控制问题。传统的编程语言中，静态类型和运行时强制执行已被用于确保程序满足用户指定的策略（如访问控制、信息流、数据来源等）。LBAC的核心思想是将