Sanjai Narain is a Chief Scientist in Information Assurance and Security at Applied Communication Sciences (formerly Telcordia Research). His current research is on planning secure and reliable cyber infrastructure. For the past three years he has led the ConfigAssure project on a science of configuration. The project builds fundamental tools for eliminating configuration errors that cause 50%-80% of vulnerabilities and downtime in cyber infrastructure. The tools exploit modern formal methods based on SAT solvers. They are being transitioned to large enterprises. He has obtained funding from government agencies and organized and led several university-industry teams. He has served on editorial boards and program committees of major journals, conferences or workshops. He joined Telcordia in 1990 when it was called Bellcore. His earlier research at Telcordia was on network management tools for SONET, ATM and DSL networks. From 1981 to 1990 he worked at RAND Corporation where he developed technologies to reason about discrete-event simulation models. His formal training is in mathematical logic, programming languages, and electrical engineering. He studied logic with Professor Alonzo Church at UCLA.

 Education

• Ph.D., Computer Science, University of California, Los Angeles, 1988

• M.S., Computer Science, Syracuse University, 1981

• B.Tech., Electrical Engineering, Indian Institute of Technology, New Delhi, 1979

Recent Projects

• Configuration-Space Randomization, 2010. CSR implements the "moving-target" defense idea. It periodically moves infrastructure from one correct configuration to another. Thereby, it invalidates an adversary's attempt at mapping out the infrastructure and planning an effective attack. Principal Investigator

• IP Assure deployment on collaboration networks, 2010. IPAssure is a non-invasive system for testing a network's security and reliability by analyzing its "DNA" in the form of component configurations. Project Manager

• Formal Methods in Networking. Graduate-level course, Computer Science Department, Princeton University, Spring 2010. Organizer and lead instructor

• Virtualization over Secure OS. HAPConfig is a new project for simplifying the configuration of the High Assurance Platform and verifying its security policy. This platform integrates VMWare with the SELinux secure operating system, 2009-2010. Principal Investigator

• Science of Configuration. ConfigAssure is a system to solve fundamental problems for bridging the gap between requirements and configuration. These are specification, synthesis, debugging, verification and reconfiguration planning. ConfigAssure uses modern constraint solvers based on those for Boolean satisfiability. System scales to infrastructure of realistic size and is being transitioned to major government enterprises, 2007-2010. Principal Investigator

• Network Planning. This project explored modern formal methods for automating DoD network planning, 2006. Principal Investigator

• Wireless Network Security. This project developed algorithms to detect malicious behavior with incomplete information in mobile ad hoc networks, 2005-2006. Researcher

• Real-time visualization of network event streams. 2009-2010. Researcher

 External collaborators in above projects are Professor Sharad Malik, Princeton, Professor Trent Jaeger, Penn State, Professor Daniel Jackson, MIT, Professor Bart Selman, Cornell, and Col. Kevin Jordan (Retd.), PACOM. Funding has been received from Telcordia Business units and government agencies such as IARPA, DARPA and DHS.

 Recent Professional Activity

• Invited Speaker, National Center for Configuration Analytics and Automation Planning Workshop, University of North Carolina, Charlotte, NC, 2011.

• Invited speaker, High Confidence Software and Systems Annual Conference, Annapolis, MD, 2011.

• Tutorial: Formal Methods For Safe Configuration of Cyberinfrastructure (with Ehab Al-Shaer). ACM Conference on Computer and Communications Security, October 7, 2010, Chicago, IL

• Thesis Committee: Realistic Evaluation of Large-Scale Distributed Systems. Richard Alimi, Computer Science Department, Yale University, September 29, 2010, New Haven, CT.

• Invited participant, Computational Cybersecurity in Compromised Environments, August 14-16, 2010, Santa Barbara, CA

• Invited speaker, International Conference on Cyber Security, August 2-5, New York, NY

• Invited speaker, NSA Trusted Computing Conference and Exposition. September 14-16, 2010. Orlando, FL

• Invited participant, Designing a Secure Systems Engineering Competition Workshop, April 6-8, 2010, Durham, NC

• Program Committee member for Internet Network Management Workshop/Workshop on Research on Enterprise Networking, collocated with USENIX, 2010.

• Formal methods for network configuration synthesis and debugging. Invited talk, Workshop on Designing Networks For Manageability. DIMACS, Rutgers University, November 12, 2009.

• Invited Participant at National Cyber Leap Year Summit, August 17-19, 2009

• Lead editor, IEEE Journal on Selected Areas in Communications (JSAC), Special Issue on Network Infrastructure Configuration, April 2009.

• Program Committee Co-Chair for Workshop on Assurable & Usable Security Configuration , Collocated with ACM Conference on Computer and Communications Security, 2009

• Invited Speaker at International Cyber Security Conference, 2009

• Program Committee member for IEEE Symposium on Policies For Distributed Systems and Networks, 2009

• Invited Panelist for National Science Foundation's Assurable and Usable Security Configuration Workshop, 2008

• Proposal Reviewer for National Science Foundation, 2008

• Program committee member for ACM Internet Network Management Workshop, in conjunction with IEEE International Conference on Network Protocols, Orlando, FL, 2008

• Program committee member for IEEE Workshop on Automated Network Management, Phoenix, AZ, 2008

• Program committee member for IEEE Policy Workshop, Palisades, NY, 2008

• Program committee member for ACM SIGCOMM Internet Network Management Workshop, Kyoto, Japan, 2007

• Program committee member for USENIX Large Installation System Administration (LISA) Conference, Dallas, TX, 2007

• Organizer, USENIX LISA Configuration Workshop, Dallas, TX, 2007

• Organizer, USENIX LISA Configuration Workshop, Washington D.C., 2006

Patents & Awards

• Method and system for estimating ability of subscriber loop to support broadband services. Awarded 2000.

• Reconfiguration planning. Filed 2010

• Verifying access-control policies with arithmetic quantifier-free form constraints. Filed 2009

• Query-based semantic analysis of ad hoc configuration languages for networks. Filed 2009

• ConfigAssure: A scalable and interactive method of generating and modifying network configurations to enforce compliance with high-level requirements. Filed 2007.

• IP network vulnerability and policy compliance assessment by IP device analysis. Filed 2007

• Network configuration management via model finding. Filed 2006.

• DARPA award given to the Dynamic Coalitions Policy Representation and Management Infrastructure project team, for technology transfer to Future Combat Systems program, 2003

• Ph.D. Thesis nominated by UCLA for ACM Distinguished Dissertation Award, 1988.

 Prior Projects

• Distributed Infrastructure Synthesis. Developed a distributed protocol for automatically synthesizing a secure and fault-tolerant virtual private network. Used group-communication protocols. Principal Investigator. 2004

• Survivable Collaboration Infrastructure. Developed a defensive architecture to ensure availability of mission-critical services in spite of attacks. Joint work with Professor Yair Amir at Johns Hopkins University, and Boeing and Sparta. Principal Investigator. 2004

• Low-Cost DSL Testing. Developed a patented system called Sapphyre for reducing DSL Loop Qualification costs by two orders of magnitude. It was used by at least 500,000 customers. 1999

• Reducing ISP/VoIP Help-Desk Cost. Designed and developed the DR. DIALUP product. This was Bellcore's first product for the consumer market. 1997.

• Alarm-Correlation for SONET/ATM networks. Developed a method of alarm correlation across protocol-layers. 1995.

• Fiber-Optic Network Interoperability Analysis. Developed a system to test compliance of SONET equipment to automatic protection switching protocol. This was used by Telcordia Professional Services for several years. 1993

• Discrete-Event Simulation. Developed DMOD, a discrete-event simulation system that allowed formal reasoning about models. 1988.

• Efficient Demand-Driven Computation. Developed an optimal method for demand-driven computation in logic for UCLA doctoral thesis. 1988.

 Selected Talks & Publications

• BGP Stable Path Problem Specification in Alloy. Formal Methods in Networking Class Note, 2010

• Network Configuration Validation. Chapter in Guide to Reliable Internet Services and Applications, edited by Chuck Kalmanek (AT&T), Richard Yang (Yale) and Sudip Misra (IIT). Springer Verlag, 2010

• Declarative Infrastructure Configuration Synthesis and Debugging. Journal of Network Systems and Management, Special Issue on Security Configuration, eds. Ehab Al-Shaer, Charles Kalmanek, Felix Wu. 2008.

• Automated Vulnerability Analysis & Mitigation in Networks. Invited talk, Computer Science Department, Naval Postgraduate School, Monterey, CA, December 6, 2007

• Invited participant, Future Internet Design Meeting, National Science Foundation, Washington, D.C., November 27-28, 2007

• Network Single Point of Failure Analysis via Model Finding. Proceedings of First Alloy Workshop, Portland, OR, November 2006.

• Network Configuration Management Via Model Finding. Proceedings of USENIX Large Installation System Administration (LISA) Conference, San Diego, CA, 2005. Also in Proceedings of ACM Workshop on Self-Managing Systems, Newport Beach, CA, 2004. Full report.

• Web Services Security Configuration Challenges. Invited paper. Workshop on Autonomic Web Computing. 47th IFIP WG 10.4 Meeting, Rincon, PR, 2005. Also at DIMACS Workshop on Web Security and E-Commerce, Rutgers University, Piscataway, NJ 2005.

• Using Service Grammar to Diagnose Configuration Errors in BGP-4. Proceedings of Usenix Systems Administrators Conference, San Diego, CA, 2003.

• Building Autonomic Systems via Configuration. Proceedings of AMS Autonomic Computing Workshop, Seattle, WA, 2003.

• Diagnosing Configuration Errors in Virtual Private Networks. Proceedings of IEEE International Communications Conference, Helsinki, Finland, 2001.

• Temporal logic. Invited article, Encyclopedia of Electrical and Electronics Engineering, ed. John Webster, John Wiley, New York, NY, 1998

• Fault-Isolation in dial-up connections. Proceedings of Fifth Hybrid Systems Conference, University of Notre Dame, Notre Dame, NY, 1997

• Proofs from temporal hypotheses via symbolic simulation. Proceedings of Hybrid Systems III, Verification and Control, eds. R. Alur, T. Henzinger, E. Sontag, Lecture Notes in Computer Science, Springer Verlag, 1996

• Proactive Network Software Maintenance. Center for Advanced Research in Networking, Bellcore, December 1995

• Alarm correlation in communication networks. Center for Advanced Research in Networking, Bellcore, December 1995

• Reasoning about hybrid systems via symbolic simulation. Proceedings of International Conference on Analysis and Optimization of Systems, INRIA, Sophia-class="SpellE"Antipolis, France, 1994

• Symbolic discrete-event simulation. Discrete-Event Systems, Manufacturing Systems and Communication Networks, eds. P. Kumar, P. Varaiya, Mathematics and its Applications, IMA volume 73, Springer Verlag, 1995

• A formal model of SONET alarm-surveillance procedures and their simulation. Proceedings of FORTE: Formal Description Techniques, Boston, MA, 1993

• Linear automatic protection switching test methodology. Proceedings of National Fiber Optics Engineering Conference, Boston, MA, 1995

• Lazy evaluation in logic programming. Proceedings of International Conference on Computer Languages, New Orleans, LA, 1990.

• Optimization by non-deterministic, lazy rewriting. Proceedings of International Conference on Rewriting Techniques & Applications, ed. N. Dershowitz, Lecture Notes in Computer Science, Springer Verlag, 1989

• A technique for doing lazy evaluation in logic. Journal of Logic Programming, Elsevier North Holland, October 1986. Also in Proceedings of IEEE Symposium on Logic Programming, Boston, MA, 1985

• Large-scale systems development in several Lisp environments. Proceedings of International Joint Conference on Artificial Intelligence, Karlsruhe, Germany, 1982

 Natural Languages

• Fluent in English, Hindi, German

 Community Service

• Member, Board of Directors, YMCA, Madison, NJ, 2000-2008

• Mentor for First Lego League team for elementary school students in Madison, NJ, 2007

• Active in Pratham, an innovative educational organization in India. A piece of photo journalism on Pratham in action.

 Hobby

• Photography, particularly portraits. Equipment: Canon 10D camera with 70-200mm/2.8L, 50mm/1.8 and 16-35mm/2.8L II lenses. For a great photography site, check out Photo.net.

 Contact

• +1 732 699 2806  (W)

• +1 908 337 3636  (M)

• snarain at appcomsci dot com