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

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

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.