=Paper=
{{Paper
|id=Vol-2019/modevva_4
|storemode=property
|title=Architecture-driven Reduction of Specification Overhead for Verifying Confidentiality in Component-based Software Systems
|pdfUrl=https://ceur-ws.org/Vol-2019/modevva_4.pdf
|volume=Vol-2019
|authors=Kateryna Yurchenko,Moritz Behr,Heiko Klare,Max Kramer,Ralf Reussner
|dblpUrl=https://dblp.org/rec/conf/models/YurchenkoBKKR17
}}
==Architecture-driven Reduction of Specification Overhead for Verifying Confidentiality in Component-based Software Systems==
https://ceur-ws.org/Vol-2019/modevva_4.pdf
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-