High-assurance synthesis of security services from basic microservices

Computer systems are vulnerable to many different types of threats ranging from harmless mistakes in data entries to malicious attacks by computer hackers. Furthermore, the explosive growth of the Internet has introduced very sophisticated ways of compromising any computer system. Consequently, a great deal of time and effort has been spent on achieving computer network security. Most of the efforts to deal with computer security have emphasized the network security aspect (i.e., the focus so far has been on intruders from outside the system). However, there also exists a significant threat from "enemies within", e.g. attacks due to malicious code embedded in the software. Whether it is intentional or not, there are many software bugs that can potentially be the source of the information misusages. One approach for dealing with this issue is to certify component security and deduce system security from its components. The advantage of this method is that it is much simpler to validate a small component as compared with a large monolithic software system. In this paper, we define a general process that allows the system security to be decomposed into orthogonal aspects so that it is possible to rigorously certify the security of a system. The approach is illustrated for the security service for an e-mail application.