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

9876058 Scott Stoller拟议的研究侧重于开发分析方法和工具，通过帮助程序员调试、系统测试和(如果可行)验证分布式软件来提高分布式软件的容错性和安全性。基于状态空间探索的验证技术只适用于有限状态系统。然而，许多分布式软件系统具有无限的参数(例如，客户端进程的数量)。拟议的研究开发了利用状态空间区域之间的部分独立性的约简，以便对有限状态系统的验证产生关于原始无界系统的结论。大多数状态空间探索工具迫使用户构建和分析软件的简化模型。建议的工具旨在分析用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.