Secure Component-Based Development of Large Software Systems

The part project "Secure Component-Based Development of Large Software Systems" is part of the Center for Research in Security and Privacy (CRISP). It is funded by the German Federal Ministry of Education and Research.

(Official CRISP website of this project)

Summary

Work Program of CRISP Part Project 1

Ensuring security in real-world complex software systems is challenging: these systems consist of a great number of interacting components, make extensive use of software libraries, and often contain weaknesses in many different abstraction layers.

This project is aimed at an answer to this challenge by providing a framework for introducing and enforcing security in the development of large complex software systems. The security-at-large paradigm shall be facilitated by its close integration into the software development process.

The resulting framework will leverage compositional analysis to combat the complexity of component-based software, will examine vulnerabilities in multiple layers to foil penetration below abstraction, and will integrate complementary methods and tools to obtain comprehensive analysis results.

The focus of this project will be on three aspects: the static security analysis of software components, the security analysis of library functions, and the dynamic security analysis of complex systems. The combination of these three aspects is essential for the effective development and verification of large software systems, and, hence, for the realization of the security-at-large paradigm.

Our Research in CRISP

Rely-guarantee-style reasoning: 

We developed rely-guarantee-style reasoning techniques for the modular and precise security verification of distributed systems where different components communicate with each other via message passing. Our development combines compositional reasoning and security type systems to ensure that there is no harmful information leakage in distributed systems. The ability to exploit assumptions in compositional security verification significantly improves the precision of the verification. Our results are currently under evaluation in a top conference.

Verification of whole-system security:

Together with the Software Technology Group at TU Darmstadt, we are developing techniques for verifying the security of whole software systems including applications and the libraries they use. The verification is compositional: the application and the libraries are analyzed isolation, and the analysis results for these two parts are combined via an interface specification. This specification is in a language developed in the spirit of RIFL.

 

Relevant Publications

A A A | Print | Imprint | Sitemap | Contact
zum Seitenanfang