Increasingly our critical infrastructures are reliant on computers. We see examples of such infrastructures in several domains, including medical, power, telecommunications, and finance. Although automation has advantages, increased reliance on computers exposes our critical infrastructures to a wider variety and higher likelihood of accidental failures and malicious attacks. Disruption of services caused by such undesired events can have catastrophic effects, such as disruption of essential services and huge financial losses. The increased reliance of critical services on our cyberinfrastructure and the dire consequences of security breaches have highlighted the importance of information security. Authorization, security protocols, and software security are three central areas in security in which there have been significant advances in developing systematic foundations and analysis methods that work for practical systems. This book provides an introduction to this work, covering representative approaches, illustrated by examples, and providing pointers to additional work in the area. Table of Contents: Introduction / Foundations / Detecting Buffer Overruns Using Static Analysis / Analyzing Security Policies / Analyzing Security Protocols

Autorentext

Anupam Datta is on the research faculty at Carnegie Mellon University. Dr. Datta's research interests are in trustworthy systems, privacy, and analysis of cryptographic protocols. He has served as General Chair of the 2008 IEEE Computer Security Foundations Symposium, Program Co-chair of the 2008 Formal and Computational Cryptography Workshop, and on the program committees of many computer security conferences including ACM CCS, IEEE S&P, and IEEE CSF. Dr. Datta has a PhD in Computer Science from Stanford University and a BTech from IIT Kharagpur. Somesh Jha received his B.Tech from Indian Institute of Technology, New Delhi in Electrical Engineering. He received his Ph.D. in Computer Science from Carnegie Mellon University in 1996. Currently, Somesh Jha is a Professor in the Computer Sciences Department at the University of Wisconsin (Madison), which he joined in 2000. His work focuses on analysis of security protocols, survivability analysis, intrusion detection, formal methods for security, and analyzing malicious code. Recently he has also worked on privacy-preserving protocols. Somesh Jha has published over 100 articles in highly-refereed conferences and prominent journals. He has won numerous best-paper awards. Somesh also received the NSF career award in 2005. Ninghui Li is an Associate Professor of Computer Science at Purdue University. He received a Bachelor's degree from the University of Science and Technology of China in 1993 and a Ph.D. in Computer Science from New York University in 2000. Before joining the faculty of Purdue in 2003, he was a Research Associate at Stanford University Computer Science Department for 3 years. Prof. Li's research interests are in computer and information security and privacy, with focuses on access control and data privacy. He has published over 90 referred papers, and has served on the Program Committees of more than 50 international conferences and workshops, including serving as the Program Chair of the 2008 ACM Symposium on Access Control Models and Technologies and the 2009 IFIP WG 11.11 International Conference on Trust Management (IFIPTM). He is on the editorial board of the VLDB Journal. His research is funded by the National Science Foundation, the Air Force Office of Scientific Research (AFOSR), the Office of Naval Research (ONR), and by IBM and Google. In 2005, he was awarded an NSF CAREER award. David Melski has been the head of the research division of GrammaTech, Inc. since 2002. Under Melski's leadership, GrammaTech Research focuses on automatic analysis and transformation of software for the purposes of reverse engineering, protection of critical IP, assurance, and producibility. GrammaTech Research employs static analysis, dynamic analysis, and combinations of static and dynamic techniques. GrammaTech Research is a leader in the development of analysis techniques both for source code and machine code. Melski received his Ph.D. in Computer Sciences from the University of Wisconsin, where his research interests included static analysis, profiling, and profile-directed optimization. Melski's Ph.D. thesis presented a framework for developing interprocedural path profiling techniques, and examined the use of path profiles for automatic program optimization. Thomas Reps is Professor of Computer Science in the Computer Sciences Department of the University of Wisconsin, which he joined in 1985. Reps is the author or co-author of four books and more than one hundred fifty papers describing his research. His research has concerned program development environments, software engineering tools, incremental graph algorithms, programanalysis algorithms, and computer security. Reps received his Ph.D. in Computer Science from Cornell University in 1982, and his Ph.D. dissertation won the 1983 ACM Doctoral Dissertation Award. Reps has been the recipient of an NSF Presidential Young Investigator Award, a Packard Fellowship, a Humboldt Research Award, and a Guggenheim Fellowship. He is also an ACM Fellow. Reps has held visiting positions at the Institut National de Recherche en Informatique et en Automatique (INRIA) in Rocquencourt, France; the University of Copenhagen, Denmark; the Consiglio Nazionale delle Ricerche (CNR) in Pisa, Italy; and the Universite Paris Diderot-Paris 7.

Inhalt
Introduction.- Foundations.- Detecting Buffer Overruns Using Static Analysis.- Analyzing Security Policies.- Analyzing Security Protocols.