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

点击翻译按钮获取中文摘要

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.