CT-ISG: Advanced Methods for Checking Information-Security Properties

威斯康星州麦迪逊大学的Reps博士提出的这个项目的目标是创造一种技术，（i）提供对计算机系统行为的更好的预测，（ii）使计算机系统更不易受到攻击。具体地说，我们提出开发改进的安全分析技术，应用于两个领域：共享计算资源的访问控制发现程序中的安全漏洞智力价值：本提案所述问题的解决办法将提供1.更好的共享计算资源访问控制方法。将解决的问题包括：在保护隐私的同时，实现跨单独管理域的协作。创建更好的方法来识别访问控制策略中的访问控制漏洞和缺陷。识别程序安全漏洞的更好的工具虽然这两个主题乍一看似乎无关，但在技术层面上它们是密切相关的：这两个领域的问题可以使用相同的机制来制定，即称为加权下推系统（WPDS）的自动机理论形式主义。WPDS求解器代表了这两个领域所需的关键算法的统一技术。因此，对WPDS和相关形式主义的研究为在这两个领域取得进展提供了智力杠杆。此外，把它们放在一起研究可能会带来额外的贝内：过去的历史表明，由一个领域的需求所推动的改进会在另一个领域产生意想不到的贝内。 更广泛的影响：随着互联网的普及，安全和可靠性问题对社会变得非常重要。每天都有新的安全漏洞被公布，电网故障是由软件错误引起的，数亿美元的太空项目被软件故障中断。更好的识别程序漏洞的工具将使软件系统具有更高的安全性和可靠性。互联网的发展也为跨组织的互动和协作提供了更好的平台。然而，互联网的去中心化本质带来了一个障碍：目前，组织维护自己的名称空间，并实施自己的访问控制策略。跨域交互可能会受到以下因素的阻碍：需要建立（全部或部分）合并各个组织的访问控制机制，以及现有名称空间和访问控制策略的结构和内容存在冲突。对共享计算资源进行访问控制的更好的方法将为支持通过因特网的跨域交互提供改进的灵活性。一个相关的目标是提供更好的方法来预测跨越组织和信任边界的访问控制策略的行为和后果。拟议的项目旨在在解决这些问题的科学和工程方面取得根本性的进展，所有这些都与NSF的Cybertrust计划的目标有关。我们的工具和实现将可供其他研究人员通过网络下载并在他们的安全分析工作。

ABSTRACT0524051Reps, ThomasU of Wisconsin MadisonThe goal of the proposed project is to create techniques that (i) provide better predictions ofthe behavior of computer systems, and (ii) make computer systems less vulnerable to attack.Speci.cally, we propose to develop improved security-analysis technology to be applied in twoareas:Access control of shared computing resourcesFinding security vulnerabilities in programsIntellectual Merit: Solutions to the problems addressed in this proposal would provide1. Better methods for access control of shared computing resources. Issues that will be addressedinclude:Enabling collaboration across separate administrative domains, while preserving privacy.Creating better methods for identifying access-control vulnerabilities and defects in accesscontrolpolicies.2. Better tools for identifying security vulnerabilities in programs.While these two topics might, at .rst blush, seem unrelated, they turn out to be closely related at thetechnical level: problems in both areas can be formulated using the same machinery an automatatheoreticformalism called weighted pushdown systems (WPDSs). WPDS solvers represent a united technology for the key algorithms required in both areas. Consequently, the study of WPDSs and related formalisms provides intellectual leverage for making advances in both areas. Moreover, studying them together is likely to bring added bene.ts: past history has shown that improvements motivated by the needs in one area have had unanticipated bene.ts in the other area. Broader Impact: As the Internet has become pervasive, security and reliability issues have become enormously important to society. New security exploits are announced daily, power-grid failures are caused by bugs in software, and multi-hundred-million-dollar space projects are interrupted by software glitches. Better tools for identifying vulnerabilities in programs will lead tosoftware systems with enhanced security and reliability.The growth of the Internet also o.ers the promise of an improved platform for cross-organizationinteraction and collaboration. However, the decentralized nature of the Internet presents an obstacle:currently, organizations maintain their own namespaces and impose their own access-control policies. Cross-domain interactions can be hindered by the need to set up access-control mechanisms that incorporate (in whole or part) those of the individual organizations, as well as by conficts in the structure and contents of existing namespaces and access-control policies. Better methods for access control of shared computing resources would provide improved .exibility for supporting cross-domain interactions via the Internet. A related objective is to provide better methods for predicting the behavior and consequences of an access-control policy that crosses organizational and trust boundaries.The proposed project aims to make fundamental advances in science and engineering that addressthese issues, all of which are relevant to the goals of NSF's Cybertrust program.Our tools and implementations will be made available for other researchers to download over theweb and use in their own security-analysis work.