Verification Techniques for Mobile Processes and Security Protocols

Ping Yang
Computer Science Department at Stony Brook University


Complex software components are playing increasingly vital roles in mission critical systems. The price of design and security flaws in these software components can range from mere economic loss to widespread service disruptions and even loss of lives. A number of verification techniques have been invented to ensure reliability and security of software systems. Model checking is one such important technique for automated verification of safety-critical systems. With mobility and security becoming integral parts of modern software systems, such as wireless and web-based applications, the ability to verify critical properties of such systems is highly important. In my thesis work, I have developed the MMC verification system, a toolset for model checking mobile systems and security protocols. MMC is applied to detect and correct flaws in the design phase of software development life cycle. In the talk, I will present the MMC verification system and the foundations that make it feasible. Then we will discuss the research challenges tackled during the development of MMC, such as optimizing compilation. Finally, I will give a brief overview of my ongoing research on compositional analysis techniques and trust management policies followed by an outline of my future research plans.