Reliably secure software systems

The security of IT-systems has obtained a crucial role. It is important for people’s everyday life, for the success of companies, and for the critical infrastructure of entire countries. The collection of data about user behavior, for instance, can help to optimize the services offered, but it also poses threats to the users’ privacy. The migration to on-line services and electronic processing can help to reduce costs, but it also increases the dependence on the availability of access to these services. Finally, electronic voting can help to simplify the casting and counting of votes, but it also raises concerns about possible manipulations of election results. The need for IT-security is reflected by the high demand for security solutions and in the annually growing security software revenues. For securing IT-systems, a wide spectrum of mechanisms is available. Authentication, access control, and cryptography canbe integrated into software to counter security threats. Firewalls, malware scanners, intrusion detection systems, and auditing can be used to provide additional protection. Such security mechanisms can be effectively used to eliminate vulnerabilities and to reduce risks of attacks. But when does a given combination of security mechanisms provide sufficient security? What are the criteria for classifying software as secure? Property-centric security complements the mechanism-centric security tradition by providing criteria for satisfactory IT-security and analysis techniques for certifying that these criteria are met. To capture security requirements, declarative security properties are employed, a prominent example being the noninterference property. This property requires that a system’s outputs to untrusted sinks must be independent from secret inputs, and it, hence, can be used to express confidentiality and privacy requirements. Program analysis is employed to check whether a given software complies with a given property. For instance, static analysis can be used to check that no secrets will be leaked by executing a program. The connection between a declarative security property and an analy-