1 Architecture-Driven Reduction of Specification Overhead for Verifying Confidentiality in Component-Based Software Systems Kateryna Yurchenko, Moritz Behr, Heiko Klare, Max Kramer and Ralf Reussner Institute for Program Structures and Data Organization Karlsruhe Institute of Technology Karlsruhe, Germany Email: firstname.lastname@kit.edu Abstract—Code verification techniques can be used confidentiality for architectural designs, developers can to guarantee that some of the information processed in account for these requirements when developing or selecting software systems remains confidential. For this, allowed components for reuse in a particular system. This can information flows have to be specified for the system under analysis. Reducing the specification overhead prevent late errors that are costly to fix. could render code verification feasible where verifica- tion was considered too complex or costly so far. In this I I . B ac kg ro u n d a n d Fo u n dat i o n s paper, we introduce a model-driven approach to reduce the overhead for creating and maintaining such speci- Before we present our approach to architecture-driven fications. Independent of the verification input format, confidentiality specifications, we briefly discuss the funda- developers can specify confidentiality for component- mental techniques that we use. based architecture models, which are kept consistent with object-oriented code. They are supported in adapt- ing the specifications to evolving systems in order to A. Component-Based Software Design detect information leaks with less effort and in earlier Our approach supports confidentiality specifications development stages. for component-based software. Components are reusable software units that provide and require services, for which I . I n t ro d u c t i o n a n d M o t i vat i o n signatures are defined in interfaces. We use the Palladio For many software systems, the confidentiality of pro- Component Model (PCM) [1] as architectural description cessed data is important. To guarantee this non-functional language. With the PCM, service signatures are modeled property, it is possible to verify the flow of information with a return type, a name, and parameters, which have a in the code. For this, confidentiality requirements have to name and a type. Confidentiality is specified based on these be specified for every system under analysis. The effort service signatures in line with the central idea of component- required to specify and verify confidentiality represents a based software development: the internal realization of design and development overhead. A part of this effort is components is hidden behind interface contracts, which inevitable, and another part is due to accidental complexity. specify properties of the input and output for provided and As a result, it is either more costly than necessary to develop required services. secure software, or the software is less secure than required. In this paper, we present an approach for reducing B. Code Generation and Consistency the overhead for creating and maintaining confidentiality Techniques to automatically derive code from models specifications using the component-based development are called code generation or model-to-text transformation paradigm and model-driven techniques. With this approach techniques. Software is, however, often not developed in 1.) confidentiality can be specified for services that are a strict forward engineering process where models are defined for component interfaces, 2.) architectural specifi- not changed after they have been used to produce code. cations for the component architecture are automatically Therefore, techniques for preserving consistency between translated into proof obligations for code verification, and code and models were developed. We use the Vitruvius 3.) evolving architectures, confidentiality specifications as framework [2] and its reactions language to keep Java code well as code are kept semi-automatically consistent with consistent with PCM instances based on monitored changes. each other. As a result, developers do not need to consider the internal realization of components or details of verifi- cation techniques. Furthermore, they can read and modify C. Specification and Verification of Confidentiality using confidentiality specifications on their level of abstraction Non-Interference because specifications in the architecture and in the code Confidentiality is specified and verified with our approach are kept consistent with each other. Finally, by specifying based on the notion of non-interference. The intuition 2 for preventing information leaks is that confidential in- C. Code Generation and Verification formation may not have any direct or indirect influence To obtain a fully functional and verified system, we on non-confidential information. For this, it has to be generate, complete, and verify code in four steps. First, specified which input data of a component’s service shall Java code and confidentiality annotations are generated not interfere. The observable behavior of the component from PCM instances and the architectural specifications. and output of the service has to be equivalent for all calls Then, the empty method stubs for component services that are equivalent with respect to this specification [3]. are manually completed. Next, the completed code with If information is classified as “high” (confidential) and confidentiality annotations is copied and the annotations “low” (non-confidential), then high inputs may not have any are translated into JML proof obligations. In this step, the observable influence on low outputs. Low inputs, however, generator produces all required JML proof obligations for may influence high outputs. In general, information can be cases that do not need to be distinguished by developers classified based on arbitrary lattices, i.e. partially ordered in architectural specifications, such as different obligations sets with unique supremum and infimum for any two for inputs and outputs to service calls. Finally, the code elements. copy is verified by proving the JML obligations using From architectural specifications we derive proof obli- KeY (subsection II-C). Figure 1 illustrates these two code gations that can be verified using the theorem prover representations of confidentiality specifications as Java KeY [4]. KeY can be used for automated and interactive annotations (middle), and as JML proof obligations (right). proofs of requirements that are expressed using dynamic The purpose of the annotations is to reduce the complexity logic and specified with the Java Modeling Language for developers by providing them a code representation of (JML) [5]. Non-interference is verified with KeY using the architectural specifications. These two representations two symbolic executions that only differ in terms of a only have syntactic differences: data set definitions are confidential input [6]. turned into Java enums and stereotype applications are I I I . A rc h i t e c t u r e - D r i v e n C o n f i d e n t i a l i t y turned into annotation usages. The level of abstraction with data sets and information flow permissions only for We will explain how confidentiality can be specified, inputs and outputs of component services is the same. verified and co-evolved in an architecture-driven way based on a simple groupware example. D. Consistency across Models and Code A. Groupware Calendar Example We introduce the intermediate annotation representation In Figure 1, we show three snippets for a groupware for confidentiality specifications not only to reduce specifi- calendar system. The first snippet shows an architectural cation complexity, but also to ease automated consistency model for a groupware component with a confidentiality preservation for it. The goal is to support development specification. The component provides a service yielding processes in which code, architectural models and confiden- all periods that are blocked by calendar entries and that tiality specifications may co-evolve. To this end, we reuse are scheduled between two given timestamps. The second a mechanism that keeps component-based architectures service yields all details for a specific calendar entry, such (PCM instances) and Java code consistent with each other as the location and participants. by reacting to monitored changes (subsection II-B). We are currently extending this mechanism to keep confiden- B. Confidentiality Specification tiality specifications on the architectural level consistent Confidentiality is not directly specified on the code level with specifications in code. The JML input for KeY is, but on the level of component-based architectures. This however, always regenerated and therefore no consistency way, developers do not need to know the verification input preservation is needed for it. format and information flow only needs to be specified for inter- but not for intra-component communication. I V . R e a l i z at i o n a n d E va l u at i o n First, so-called data sets have to be defined. They group In our prototypical implementation1 , data set definitions data that may interfere with each other but not with other and pairs that link data sets and parameters or return values data sets. If information may flow from and to these data are persisted in a confidentiality specification model that sets, it is specified for service signatures of architectural is kept separate from the architectural models. Stereotypes interfaces. Other flows are not permitted. of a confidentiality profile for PCM can be applied to In our example in Figure 1, confidentiality specifica- service signatures of architectural interfaces in order to tions are shown as notes with the keyword includes. For refer to these pairs as tagged values. By using this non- the service getBlockedPeriods, a star yields two allowed invasive profile mechanism the architecture models remain information flows: 1.) non-confidential information (low) compatible to all Palladio tooling. may influence all inputs, 2.) returned values may influence To obtain Java code and confidentiality annotations low information. For the service getFullCalendarEntry, from PCM instances and specifications, we have created a it is specified that 1.) low information may influence generator based on Xtend. An additional generator for JML the provided ID, 2.) returned values may only influence confidential information (high). 1 github.com/KASTEL-SCBS/PCM2Java4Key 3 //@ model \seq metadata; enum DataSets {APPOINTMENT(),METADATA();} //@ \determines this.getBlockedPeriods(\result) enum IFPairs { //@ \by this.getBlockedPeriods(from), METADATA_STAR(DataSets.METADATA,"*"), //@ this.getBlockedPeriods(to) METADATA_ID(DataSets.METADATA,"id"), //@ \preserving metadata; APP_RETURN(DataSets.APPOINTMENT,"\return"); BP[] getBlockedPeriods(TS from, TS to) {...} } //@ model \seq metadata; interface Calendar { //@ \by this.getFullCalendarEntry(id) @NISPEC({IFPairs.METADATA_STAR}) //@ \preserving metadata; BP[] getBlockedPeriods(TS from, TS to); //@ model \seq appointment; @NISPEC({IFPairs.METADATA_ID, IFPairs.APP_RETURN}) //@ \determines this.getFullCalendarEntry(\result) CE getFullCalendarEntry(ID id); //@ \preserving appointment; } CE getFullCalendarEntry(ID id) {...} Figure 1. Architectural model and specification (left), Java code with annotations (middle), and JML comments (right) for a groupware calendar example proof obligations is under development. Both generators dentiality specifications for the verification of component- process the complete input in batch mode and overwrite based software. We have presented architecture-driven con- previous output. We are currently developing consistency fidentiality specifications for which JML proof obligations preservation reactions, which update annotations after can be automatically derived so that developers do not changes in architectural specifications. Java code and need to know the verification input. Furthermore, we have architectural models are already kept consistent based on proposed a mechanism for keeping evolving architectures, previous work [2]. confidentiality specifications and code consistent with each To ensure the quality of both batch generators and of the other. With it, developers can design and realize software incremental reactions, we create unit tests that compare with confidential data in an incremental way and on their the obtained output with expected outputs for all types of level of abstraction. The goal of the approach is to help specification possibilities and changes. Furthermore, we will developers in finding confidentiality leaks with less overhead perform cross-validation by always comparing the result of and in earlier development stages. incremental consistency preservation with that of a batch generation of code and annotations. References We will evaluate how confidentiality can be specified [1] R. H. Reussner, S. Becker, J. Happe, R. Heinrich, A. Koziolek, and maintained in an architecture-driven way using three H. Koziolek, M. Kramer, and K. Krogmann, Modeling and systems: a simple web shop, a cloud-based file sharing Simulating Software Architectures – The Palladio Approach. Cambridge, MA: MIT Press, 2016, 408 pp. platform, and a common case study realizing a trading [2] M. E. Kramer, M. Langhammer, D. Messinger, S. Seifermann, system for retail shops. and E. Burger, “Change-driven consistency for compo- nent code, architectural models, and contracts,” in 18th V . R e l at e d Wo r k International Symposium on Component-Based Software Jürjens presents a model-driven approach where security- Engineering, ser. CBSE ’15, Montréal, QC, Canada: ACM, 2015, pp. 21–26. relevant information is specified on the system design level [3] S. Greiner and D. Grahl, “Non-interference with what- using the UMLsec extension for the Unified Modeling declassification in component-based systems,” in 2016 IEEE Language (UML) [7]. This approach does, however, not 29th Computer Security Foundations Symposium (CSF), support automatic proof obligations generation for code. 2016, pp. 253–267. The IFlow approach [8] allows the model-driven develop- [4] B. Beckert, R. Hähnle, and P. H. Schmitt, Eds., Verification ment of distributed systems consisting of mobile apps and of Object-Oriented Software: The KeY Approach, ser. LNCS 4334. Springer-Verlag, 2007. web services which are secure w.r.t. information flow. Using [5] G. T. Leavens, A. L. Baker, and C. Ruby, “Preliminary the system’s UML model, IFlow automatically generates design of jml: A behavioral interface specification language code and a formal model of the system based on abstract for java,” ACM SIGSOFT Software Engineering Notes, 31, state machines, which is used to verify information-flow no. 3, pp. 1–38, 2006. properties. IFlow does not support automatic consistency [6] C. Scheben and S. Greiner, “Information flow analysis,” preservation on both design and code levels during the in Deductive Software Verification – The KeY Book: From Theory to Practice, W. Ahrendt, B. Beckert, R. Bubel, R. system evolution. Hähnle, P. H. Schmitt, and M. Ulbrich, Eds. Cham: Springer To the best of our knowledge, there is no other approach International Publishing, 2016, pp. 453–471. for verifying component-based software against architec- [7] J. Jürjens, “Umlsec: Extending uml for secure systems tural confidentiality requirements or for preserving con- development,” in International Conference on The Unified sistency between confidentiality specifications in software Modeling Language, Springer, 2002, pp. 412–425. architecture descriptions and code. [8] K. Katkalov, K. Stenzel, M. Borek, and W. Reif, “Model- driven development of information flow-secure systems with iflow,” in Social Computing (SocialCom), 2013 International VI. Conclusions Conference on, IEEE, 2013, pp. 51–56. In this paper, we have presented a model-driven approach that facilitates the creation and maintenance of confi-