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

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

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.