CAREER: Automated Analysis of Security and Fault-Tolerance of Distributed Systems

职业：分布式系统安全性和容错性的自动分析

• 批准号: 9876058
• 负责人: Scott Stoller
• 金额: $ 20.5万
• 依托单位: Indiana University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 1999
• 资助国家: 美国
• 起止时间: 1999-08-01 至 2001-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=9876058&HistoricalAwards=false
• 关键词: CAREER; Automated; Analysis; Security; Fault

9876058 Scott Stoller The proposed research focuses on the development of analysis methods and tools that increase the fault-tolerance and security of distributed software by helping programmers to debug, systematically test, and (when feasible) verify such software. Verification techniques based on state-space exploration apply directly only to finite-state systems. However, many distributed software systems have unbounded parameters (e.g., the number of client processes). The proposed research develops reductions that exploit partial independence between regions of the state space, so that verification of a finite-state system yields conclusions about the original unbounded system. Most state-space exploration tools force the user to construct and analyze simplified models of software. The proposed tool aims to analyze programs written in general-purpose languages, such as Java. The tool's basic design follows that of VeriSoft: state-space exploration is performed without storing the set of visited states, with optimizations to reduce the redundant computation (multiple visits to a state) that this may cause. The proposed research extends this approach to handle systems that use cryptography. Software used in undergraduate and graduate operating systems courses will be enhanced with the form of state-space exploration just described, providing students with powerful support for finding synchronization errors and other bugs.

9876058 Scott Stoller提出的研究重点是开发分析方法和工具，通过帮助程序员调试、系统测试和（在可行的情况下）验证这些软件来增加分布式软件的容错性和安全性。基于状态空间探索的验证技术只直接适用于有限状态系统。然而，许多分布式软件系统具有无限参数（例如，客户端进程的数量）。提出的研究开发了利用状态空间区域之间的部分独立性的约简，以便对有限状态系统的验证产生关于原始无界系统的结论。大多数状态空间探索工具都迫使用户构建和分析简化的软件模型。该工具旨在分析用通用语言（如Java）编写的程序。该工具的基本设计遵循VeriSoft：执行状态空间探索时不存储访问过的状态集，并进行优化以减少可能导致的冗余计算（多次访问一个状态）。本研究将此方法扩展到使用密码学的系统。本科和研究生操作系统课程中使用的软件将以刚才描述的状态空间探索的形式得到加强，为学生发现同步错误和其他错误提供强大的支持。