Secure Programming via Visibly Pushdown Safety Games

Secure Programming via Visibly Pushdown Safety Games
复制标题

通过明显的下推安全游戏进行安全编程

DOI:
--
复制
发表时间:
2012
期刊:
International Conference on Computer Aided Verification
影响因子:
--
通讯作者:
T. Reps
T. Reps
中科院分区:
--
文献类型:
--
作者:
William R. Harris;S. Jha;T. Reps

文献摘要

被引文献

相似文献

最近的几个操作系统提供了系统调用,允许应用程序显式地管理与应用程序交互的模块的权限。这样的入侵检测感知操作系统允许程序员编写满足强安全策略的程序,即使它与不受信任的模块交互。然而,重写程序以正确地使用系统调用来满足高级安全策略通常是不平凡的。本文讨论的策略编织问题是以一个程序、一个期望的高级策略和一个系统调用如何影响特权的描述作为输入,自动重写程序以调用系统调用,使其满足策略。我们提出了一种算法,解决了策略编织问题,减少它找到一个获胜的模块化策略,以一个明显的下推安全游戏,并适用于一种新的游戏求解算法产生的游戏。实验结果表明,该算法可以有效地重写实际的程序,为一个实际的入侵检测系统。
Several recent operating systems provide system calls that allow an application to explicitly manage the privileges of modules with which the application interacts. Such privilege-aware operating systems allow a programmer to a write a program that satisfies a strong security policy, even when it interacts with untrusted modules. However, it is often non-trivial to rewrite a program to correctly use the system calls to satisfy a high-level security policy. This paper concerns the policy-weaving problem, which is to take as input a program, a desired high-level policy for the program, and a description of how system calls affect privilege, and automatically rewrite the program to invoke the system calls so that it satisfies the policy. We present an algorithm that solves the policy-weaving problem by reducing it to finding a winning modular strategy to a visibly pushdown safety game, and applies a novel game-solving algorithm to the resulting game. Our experiments demonstrate that our algorithm can efficiently rewrite practical programs for a practical privilege-aware system.