Tutorial 4
Date/Time: Thursday 7th, 2010 13:30pm -- 16:30pm
Duration: 3 hours
Title: Formal Methods for Safe Configuration of Cyberinfrastructure
Presenters: Sanjai Narain (Telcordia Technologies) and Ehab Al Shaer (UNC Charlotte)
Abstract:
Configuration is the glue for logically integrating components to satisfy end-to-end requirements on cyberinfrastructure. Today, the large gap between requirements and configurations is manually bridged. As a result, large numbers of configuration errors are made. It is well-documented that such errors are responsible for 50%-80% of infrastructure vulnerabilities and downtime. This tutorial covers the fundamental problems of discovering and eliminating security misconfigurations: specification, diagnosis, repair, synthesis, verification and reconfiguration planning. The tutorial surveys modern formal methods, namely, Binary Decision Diagrams (BDDs), SAT solvers, SMT solvers, Prolog and Datalog and shows how they have been applied to solve the above problems. The tutorial also discusses experience with applying these solutions to real infrastructure: an enterprise network, a high-performance data center, virtual private networks for collaboration, and a platform that integrates virtualization with a secure operating system.
Bios:Dr. Sanjai Narain is a Senior Research Scientist in Information Assurance and Security at Telcordia Technologies, Inc. His current research is on fundamental tools for designing and implementing secure and reliable network infrastructure. For the past three years he has led the ConfigAssure project on a science of configuration, in collaboration with MIT, Princeton and Penn State. His research is funded by government agencies and is being transitioned to major enterprises. In Spring of 2010 he organized a graduate-level course "Formal Methods in Networking" at Princeton. He joined Telcordia in 1990 when it was called Bellcore. His earlier research at Telcordia was on tools for managing SONET, ATM and DSL networks. From 1981 to 1990 he worked at RAND Corporation on techniques to reason about discrete event simulation. His formal training is in Electrical Engineering, Computer Science, Programming Languages and Mathematical Logic. He obtained a B.Tech from Indian Institute of Technology, New Delhi, in 1979, an M.S. from Syracuse University, in 1981, and a Ph.D. from University of California, Los Angeles, in 1988.
Dr. Ehab Al-Shaer is an Associate Professor and the Director of the Cyber Defense and Network Assurability (CyberDNA) Center in the School of Computing and Informatics at University of North Carolina Charlotte. His primary research areas are network security, security management, fault diagnosis, and network assurability. He is the General Chair of ACM Computer and Communication, 2009-2010 and NSF Workshop in Assurable and Usable Security Configuration, 2008. He has also served as a Workshop Chair and Program Co-Chair for a number of well established conferences and workshops in his area. He received his M.S. in Computer Science from Northeastern University, Boston, MA in 1994 and his Ph.D. in Computer Science from Old Dominion University, Norfolk, VA, in 1998.
Last modified: 2010-09-02 00:02:54 EDT