Cache Side-Channel Attacks (CSCAs) can leak sensitive information by exploiting shared cache resources. Although many secure cache designs like CEASER, ScatterCache, PhantomCache, MIRAGE, and IECache have been proposed, the security evaluation methods being used by these designs remain diverse, often inconsistent, and scattered. This inconsistency makes it challenging to compare the security strengths of the state-of-the-art cache designs for security-critical applications. To address this challenge, we propose a novel consistent security evaluation methodology, called the UniSEC (Unified methodology for Security Evaluation of Caches), which estimates Worst-Case Leakage (WCL) and provides a consistent, comprehensive, and realistic measure of potential information leakage that various cache designs exhibit. UniSEC empirically shows that WCL estimation maximizes the revelation of potential information leakage that Relative Eviction Entropy (REE) based method fails to capture. UniSEC introduces an Effective Security Score (ESS) that takes into account Active Attacker’s Cache Lines (AACLs) within an attacker’s eviction set and the uniformity of the eviction distribution across the AACLs to measure the worst-case leakage. Our results show that well-distributed eviction probabilities across attacker’s eviction set lead to higher ESS and overall entropy. We carry out experiments to measure WCL, REE, and ESS in six state-of-the-art secure cache designs and vary associativity and cache sizes to measure the impact on information leakage. Our experiments reveal that security-critical applications cannot rely on the security guarantees being provided by REE alone. Therefore, WCL is a more realistic metric for measuring the actual amount of information leakage in caches.

We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs arguing for why and how does every computer science graduate benefit from such knowledge. We do not agree with the sentence “While there is a belief that formal methods are important and they are growing in importance, we cannot state that every computer science graduate will need to use formal methods in their career.” We argue that formal methods are and have to be an integral part of every computer science curriculum. Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently. The same way, students have to understand why and how formal methods work, what their formal background is, and how they are justified. No engineer should be ignorant of the foundations of their subject and the formal methods based on these. In this article, we aim at highlighting why every computer scientist needs to be familiar with formal methods. We argue that education in formal methods plays a key role by shaping students' programming mindset, fostering an appreciation for underlying principles, and encouraging the practice of thoughtful program design and justification, rather than simply writing programs without reflection and deeper understanding. Since integrating formal methods into the computer science curriculum is not a straightforward process, we explore the additional question: what are the tradeoffs between one dedicated knowledge area of formal methods in a computer science curriculum versus having formal methods scattered across all knowledge areas? Solving problems while designing software and software-intensive systems demands an understanding of what is required, followed by a specification and formalizing a solution in a programming language. How to do this systematically and correctly on solid grounds is exactly supported by formal methods.

Smart contracts are computer programs designed to automate legal agreements. They are usually developed in a high-level programming language, the most popular of which is Solidity. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars’ worth of transactions. As for every computer program, smart contracts may contain bugs which can be exploited. However, since smart contracts are often used to automate financial transactions, such exploits may result in huge economic losses. In general, it is estimated that since 2019, more than $5B was stolen due to vulnerabilities in smart contracts. This article addresses the issue of smart contract vulnerabilities by introducing an executable denotational semantics for Solidity within the Isabelle/HOL interactive theorem prover. This formal semantics serves as the basis for an interactive program verification environment for Solidity smart contracts. To evaluate our semantics, we integrate grammar-based fuzzing with symbolic execution to automatically test it against the Solidity reference implementation. The article concludes by showcasing the formal verification of Solidity programs, exemplified through the verification of a basic Solidity token.

In protocol verification, we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants such as Isabelle/HOL. The latter provides overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely, and thus the risk of erroneously verifying a flawed protocol is nonnegligible. There are a few works that try to combine the advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step toward achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge, this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results, such as the soundness of a typed model.

Isabelle/DOF is an ontology framework on top of Isabelle/HOL. It allows for the formal development of ontologies and continuous conformity-checking of integrated documents, including the tracing of typed meta-data of documents. Isabelle/DOF deeply integrates into the Isabelle/HOL ecosystem, allowing to write documents containing (informal) text, executable code, (formal and semiformal) definitions, and proofs. Users of Isabelle/DOF can either use HOL or one of the many formal methods that have been embedded into Isabelle/HOL to express formal parts of their documents. In this paper, we extend Isabelle/DOF with annotations of -terms, a pervasive data-structure underlying Isabelle to syntactically represent expressions and formulas. We achieve this by using Higher-order Logic (HOL) itself for query-expressions and data-constraints (ontological invariants) executed via code-generation and reflection. Moreover, we add support for parametric ontological classes, thus exploiting HOL's polymorphic type system. The benefits are: First, the HOL representation allows for flexible and efficient run-time checking of abstract properties of formal content under evolution. Second, it is possible to prove properties over generic ontological classes. We demonstrate these new features by a number of smaller ontologies from various domains and a case study using a substantial ontology for formal system development targeting certification according to CENELEC 50128.

ABSTRACT Modern supply chains of goods and services rely heavily on close collaborations between the partners within these supply chains. Consequently, there is a demand for IT systems that support collaborations between business partners, for instance, allowing for joint computations for global optimizations (in contrast to local optimizations that each partner can do on their own). Still, businesses are very reluctant to share data or connect their enterprise systems to allow for such joint computation. The topmost factor that businesses name as reason for not collaborating, is their security concern in general and, in particular, the confidentiality of business critical data. While there are techniques (e.g., homomorphic encryption or secure multiparty computation) that allow joint computations and, at the same time, that are protecting the confidentiality of the data that flows into such a joint computation, they are not widely used. One of the main problems that prevent their adoption is their perceived performance overhead. In this paper, we address this problem by an approach that utilized the structure of supply chains by decomposing global computations into local groups, and applying secure multiparty computation within each group. This results in a scalable (resulting in a significant smaller runtime overhead than traditional approaches) and secure (i.e., protecting the confidentiality of data provided by supply chain partners) approach for joint computations within supply chains. We evaluate our approach using life‐cycle assessment (LCA) as a case study. Our experiments show that, for instance, secure LCA computations even in supply chains with 15 partners are possible within less than two minutes, while traditional approaches using secure multiparty computation need more than a day.

Deep learning models are intrinsically susceptible to textual adversarial attacks on social media, where the perturbed text can trigger aberrant behaviours of victim models and threaten security and privacy. In this paper, we present a novel word-level attack called SCALA: a Synonym-based desCending And repLace-back Ascending mechanism. Our focus is on the efficient production of adversarial examples, with a particular emphasis on minimizing human perceptibility while ensuring the visual resemblance and semantic correctness. The merits of our attacking solution lie in being:(i)imperceptible – it keeps a very low word perturbation rate based on the Hamming (L0-norm) distance, thus achieving heightened deceptiveness validated through human evaluations;(ii)efficient – our tensor-based parallelization strategy ensures the attacking efficiency compared with baselines;(iii)effective – it surpasses seven state-of-the-art attacks on five target models in terms of reducing after-attack accuracy;(iv)practical – black-box score-based setting ensures that the adversary only needs to query target models for confidence scores; and(v)transferable – our attack shows competitive transferability on the generated adversarial examples. We release our codeSCALAvia https://github.com/TrustAI/SCALA.

Communication networks like the Internet form a large distributed system where a huge number of components run in parallel, such as security protocols and distributed web applications. For what concerns security, it is obviously infeasible to verify them all at once as one monolithic entity; rather, one has to verify individual components in isolation. While many typical components like TLS have been studied intensively, there exists much less research on analyzing and ensuring the security of the composition of security protocols. This is a problem since the composition of systems that are secure in isolation can easily be insecure. The main goal of compositionality is thus a theorem of the form: given a set of components that are already proved secure in isolation and that satisfy a number of easy-to-check conditions, then also their parallel composition is secure. Said conditions should of course also be realistic in practice, or better yet, already be satisfied for many existing components. Another benefit of compositionality is that when one would like to exchange a component with another one, all that is needed is the proof that the new component is secure in isolation and satisfies the composition conditions—without having to re-prove anything about the other components. This article has three contributions over previous work in parallel compositionality. First, we extend the compositionality paradigm to stateful systems : while previous approaches work only for simple protocols that only have a local session state, our result supports participants who maintain long-term databases that can be shared among several protocols. This includes a paradigm for declassification of shared secrets . This result is in fact so general that it also covers many forms of sequential composition as a special case of stateful parallel composition. Second, our compositionality result is formalized and proved in Isabelle/HOL, providing a strong correctness guarantee of our proofs. This also means that one can prove, without gaps, the security of an entire system in Isabelle/HOL, namely the security of components in isolation and the composition conditions, and thus derive the security of the entire system as an Isabelle theorem. For the components one can also make use of our tool PSPSP that can perform automatic proofs for many stateful protocols. Third, for the compositionality conditions we have also implemented an automated check procedure in Isabelle.

In protocol verification we observe a wide spectrum from fully automated methods to interactive theorem proving with proof assistants like Isabelle/HOL. The latter provide overwhelmingly high assurance of the correctness, which automated methods often cannot: due to their complexity, bugs in such automated verification tools are likely and thus the risk of erroneously verifying a flawed protocol is non-negligible. There are a few works that try to combine advantages from both ends of the spectrum: a high degree of automation and assurance. We present here a first step towards achieving this for a more challenging class of protocols, namely those that work with a mutable long-term state. To our knowledge this is the first approach that achieves fully automated verification of stateful protocols in an LCF-style theorem prover. The approach also includes a simple user-friendly transaction-based protocol specification language embedded into Isabelle, and can also leverage a number of existing results such as soundness of a typed model

Free and Open Source Software (FOSS) components are ubiquitous in both proprietary and open source applications. Each time a vulnerability is disclosed in a FOSS component, a software vendor using this component in an application must decide whether to update the FOSS component, patch the application itself, or just do nothing as the vulnerability is not applicable to the older version of the FOSS component used. This is particularly challenging for enterprise software vendors that consume thousands of FOSS components and offer more than a decade of support and security fixes for their applications. Moreover, customers expect vendors to react quickly on disclosed vulnerabilities-in case of widely discussed vulnerabilities such as Heartbleed, within hours. To address this challenge, we propose a screening test: a novel, automatic method based on thin slicing, for estimating quickly whether a given vulnerability is present in a consumed FOSS component by looking across its entire repository. We show that our screening test scales to large open source projects (e.g., Apache Tomcat, Spring Framework, Jenkins) that are routinely used by large software vendors, scanning thousands of commits and hundred thousands lines of code in a matter of minutes. Further, we provide insights on the empirical probability that, on the above mentioned projects, a potentially vulnerable component might not actually be vulnerable after all.

Abstract Service composition is a key concept of Service‐Oriented Architecture that allows for combining loosely coupled services that are offered and operated by different service providers. Such environments are expected to dynamically respond to changes that may occur at runtime, including changes in the environment and individual services themselves. Therefore, it is crucial to monitor these loosely coupled services throughout their lifetime. In this paper, we present a novel framework for monitoring services at runtime and ensuring that services behave as they have promised. In particular, we focus on monitoring non‐functional properties that are specified within an agreed security contract. The novelty of our work is based on the way in which monitoring information can be combined from multiple dynamic services to automate the monitoring of business processes and proactively report compliance violations. The framework enables monitoring of both atomic and composite services and provides a user friendly interface for specifying the monitoring policy. We provide an information service case study using a real composite service to demonstrate how we achieve compliance monitoring. The transformation of security policy into monitoring rules, which is done automatically, makes our framework more flexible and accurate than existing techniques.

Finding and fixing software vulnerabilities have become a major struggle for most software development companies. While generally without alternative, such fixing efforts are a major cost factor, which is why companies have a vital interest in focusing their secure software development activities such that they obtain an optimal return on this investment. We investigate, in this paper, quantitatively the major factors that impact the time it takes to fix a given security issue based on data collected automatically within SAP’s secure development process, and we show how the issue fix time could be used to monitor the fixing process. We use three machine learning methods and evaluate their predictive power in predicting the time to fix issues. Interestingly, the models indicate that vulnerability type has less dominant impact on issue fix time than previously believed. The time it takes to fix an issue instead seems much more related to the component in which the potential vulnerability resides, the project related to the issue, the development groups that address the issue, and the closeness of the software release date. This indicates that the software structure, the fixing processes, and the development groups are the dominant factors that impact the time spent to address security issues. SAP can use the models to implement a continuous improvement of its secure software development process and to measure the impact of individual improvements. The development teams at SAP develop different types of software, adopt different internal development processes, use different programming languages and platforms, and are located in different cities and countries. Other organizations, may use the results—with precaution—and be learning organizations.

Summary In the world of large‐scale applications, software as a service (SaaS) in general and use of microservices, in particular, is bringing service‐oriented architectures to a new level: Systems in general and systems that interact with human users (eg, sociotechnical systems) in particular are built by composing microservices that are developed independently and operated by different parties. At the same time, SaaS applications are used more and more widely by enterprises as well as public services for providing critical services, including those processing security or privacy of relevant data. Therefore, providing secure and reliable service compositions is increasingly needed to ensure the success of SaaS solutions. Building such service compositions securely is still an unsolved problem. In this paper, we present a framework for modelling, validating, and ranking secure service compositions that integrate both automated services as well as services that interact with humans. As a unique feature, our approach for ranking services integratesvalidated properties(eg, based on the result of formally analysing the source code of a service implementation) as well ascontractual propertiesthat are part of the service level agreement and, thus, not necessarily ensured on a technical level.

Firewalls are an important means to secure critical ICT infrastructures. As configurable off-the-shelf products, the effectiveness of a firewall crucially depends on both the correctness of the implementation itself as well as the correct configuration. While testing the implementation can be done once by the manufacturer, the configuration needs to be tested for each application individually. This is particularly challenging as the configuration, implementing a firewall policy, is inherently complex, hard to understand, administrated by different stakeholders and thus difficult to validate. This paper presents a formal model of both stateless and stateful firewalls (packet filters), including NAT, to which a specification-based conformance test case generation approach is applied. Furthermore, a verified optimisation technique for this approach is presented: starting from a formal model for stateless firewalls, a collection of semantics-preserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage of the model are derived. We extend an existing approach that integrates verification and testing, that is, tests and proofs to support conformance testing of network policies. The presented approach is supported by a test framework that allows to test actual firewalls using the test cases generated on the basis of the formal model. Finally, a report on several larger case studies is presented. Copyright © 2014 John Wiley & Sons, Ltd.

The increasing use of IT systems in security or safety critical areas as well as growing system complexity creates challenges for both formal verification and testing. It might initially appear that these are competing techniques: it can be argued that once a program is proven to be correct, there is no need for additional tests. Similarly, if it is not feasible to produce a formal proof, then one cannot do better than testing your program thoroughly. As a consequence of this perception, proofs and tests have been pursued by distinct communities using rather different techniques and tools. Despite this historical separation of work on testing and proof, research in these areas has led to the discovery of common issues and to the realisation that each may need the other. The emergence of model checking was one of the first signs that contradictions contribute to testing, but in the past few years an increasing number of researchers have encountered the need to combine proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer. This special issue of STVR tries to bring together researchers and practitioners working in the converging fields of testing and proving. We received 16 submissions for this special issue. Reviewing followed the same process as for regular papers. Each paper was reviewed by at least three reviewers, and after a rigorous selection process requiring a total of 33 revisions and 75 reviews, seven papers remain for publication. These papers are spread across two special issues of STVR and discuss two different aspects of tests and proofs: model-based testing and approaches for improving the quality of generated test data. This first volume includes the first three papers, covering the use of tests and proof in model-based testing. The first paper, “Test generation with SMT solvers in Model-Based Testing” by Jérôme Cantenot, Fabrice Ambert, and Fabrice Bouquet presents a framework for generating test cases from a subset of UML (class models, object models, and state modes) that are enriched with constraints expressed in OCL. The developed test generation methods ensure that each operation and transition of the model is stimulated at least once during test execution. The second paper, “Test Generation from Recursive Tile Systems” by Sébastien Chédor, Thierry Jéron, and Christophe Morvan explores the generation of conformance test cases from recursive tile systems models. The authors discuss both on-line and off-line test cases for recursive tile systems within the ioco framework. The third paper, “Model Based Testing for Concurrent Systems with Labeled Event Structures” by Hernán Ponce de León, Stefan Haar, and Delphine Longuet presents a model-based approach for testing concurrent systems. The concurrent systems are modeled using labeled event structures and their test case generation algorithm is able to derive a sound and exhaustive test suite from these models. All the contributions presented in this and the upcoming special issue on Tests and Proofs reveal the broad and dynamic community that works on the intersection of tests and proofs. This was only possible through the combined efforts of all authors and reviewers, and we wish to thank them all for their time and energy. The following persons were reviewers: Paul Ammann, Lukas Brügger, Fabian Büttner, Cristian Cadar, George Candea, John Derrick, Catherine Dubois, Alessandro Fantechi, Vijay Ganesh, Angelo Gargantini, Ryszard Janicki, Thierry Jéron, Tomoji Kishi, Nils Klarlund, Nikolai Kosmatov, Moez Krichen, Pascale Le Gall, Bruno Legeard, Zdenek Letko, Xuandong Li, Karl Meinke, Magnus Myreen, Joseph Near, Virginia Papailiopoulou, Jan Peleska, Dennis Peters, Alexander Pretschner, Antoine Rollet, Kristin Y. Rozier, Andy Schurr, Thomas Sewell, Tomohiko Takagi, Andreas Teucke, T.H. Tse, Mark Utting, Machiel van der Bijl, Luca Viganò, Birgit Vogel-Heuser, Tjark Weber, Stephan Weissleder, Tim A.C. Willemse, Christoph Wintersteiger, Burkhart Wolff, Dianxiang Xu, and Steve Zdancewic. Last but not least, the STVR chief editors, Robert Hierons and Jeff Offutt, provided expert guidance and important advice throughout the process.

In our continued effort to reduce the backlog of accepted papers at STVR, this issue has six papers. The first four make up volume 2 of the special issue on tests and proofs, and the last two are regular papers. I introduce the two regular papers here, and the special issue editors introduce the special issue papers below. "A model-free and state-cover testing scheme for semaphore-based and shared-memory concurrent programs," by Gwan-Hwan Hwang, Che-Sheng Lin, Teng-Shuo Lee, and Chi Wu-Lee, addresses the testing of concurrent programs. If the number of synchronization sequences is finite, their approach tests all of them, If the number of synchronization sequences is infinite, their approach applies state-cover testing. (Recommended by Marc Roper.) "Exploring the missing link: An empirical study of software fixes," by Maggie Hamill and Katerina Goseva-Popstojanova, gives data from a study of fixes to software faults. They used a safety-critical NASA program and report, among other findings, that a significant percentage of fixes required changes to multiple modules. (Recommended by Jane Hayes.) I would also like to take this opportunity to thank the special issue editors, Achim Brucker and Jacques Julliand, for their incredible hard work and dedication in putting this special issue together. The increasing use of IT systems in security or safety critical areas as well as the growing system complexity creates challenges for both formal verification and testing. It might initially appear that these are competing techniques: it can be argued that once a program is proven to be correct, there is no need for additional tests. Similarly, if it is not feasible to produce a formal proof, then one cannot do better than testing your program thoroughly. As a consequence of this perception, proofs and tests have been pursued by distinct communities using rather different techniques and tools. Despite this historical separation of work on testing and proof, research in these areas has led to the discovery of common issues and to the realisation that each may need the other. The emergence of model checking was one of the first signs that contradictions contribute to testing, but in the past few years an increasing number of researchers have encountered the need to combine proofs and tests, dropping earlier dogmatic views of incompatibility and taking instead the best of what each of these software engineering domains has to offer. This special issue of STVR tries to bring together researchers and practitioners working in the converging fields of testing and proving. We received 16 submissions for this special issue. Reviewing followed the same process as for regular papers. Each paper was reviewed by at least three reviewers, and after a rigorous selection process requiring a total of 33 revisions and 75 reviews, seven papers remain for publication. These papers are spread across two special issues of STVR and discuss two different aspects of tests and proofs: model-based testing, and approaches for improving the quality of generated test data. This is the second volume of the Special Issue on Tests and Proofs. The four papers in this issue discuss techniques for improving the generation time and quality of test data sets. The first paper, “Bridging the Gap Between Easy Generation and Efficient Verification of Unsatisfiability Proofs” by Marijn J. H. Heule, Warren A. Hunt Jr., and Nathan Wetzler proposes a new format for refutation proofs of SAT solvers that allows for clause deletion during proof checking. Among others, the work of the authors facilitates unsatisfiability checking and makes it possible to efficiently integrate results of a SAT solver in a logical safe way into proof techniques. The second paper, “Automated Test Case Generation for FBD Programs Implementing Reactor Protection System Software” by Eunkyoung Jee, Donghwan Shin, Sungdeok Cha, Jang-Soo Lee and Doo-Hwan Bae presents an approach that uses SAT solvers during test case generation to improve its efficiency and its reliability. In particular, the authors present an approach for automatically generating test cases that check correctness relative to functional block diagrams, a formalism used in implementing safety critical systems. The third paper, “RepOK-Based Reduction of Bounded-Exhaustive Testing” by Valeria Bengolea, Nazareno Aguirre, Darko Marinov, and Marcelo Frias, presents techniques for reducing the time for bounded-exhaustive testing, by either reducing the generation time or reducing the obtained bounded-exhaustive suites, e.g., by removing those tests that are equivalent to some tests already present in the suite. The fourth paper, “A Random Testing Approach Using Pushdown Automata” by Aloïs Dreyfus, Pierre-Cyrille Héam, Olga Kouchnarenko, and Catherine Masson, addresses the problem that generating test cases from abstract models may result in tests that are not concretisable, i.e., do not correspond to an actual execution of the system under test. The pushdown automata-based approach of the authors has, compared to approaches from the literature, a much higher ability to generate concretisable test cases. All the contributions presented in this issue and the previous special issue on Tests and Proofs reveal the broad and dynamic community that works on the intersection of tests and proofs. This was only possible through the combined efforts of all authors and reviewers, and we wish to thank them all for their time and energy. The following persons were reviewers: Paul Ammann, Lukas Brügger, Fabian Büttner, Cristian Cadar, George Candea, John Derrick, Catherine Dubois, Alessandro Fantechi, Vijay Ganesh, Angelo Gargantini, Ryszard Janicki, Thierry Jéron, Tomoji Kishi, Nils Klarlund, Nikolai Kosmatov, Moez Krichen, Pascale Le Gall, Bruno Legeard, Zdenek Letko, Xuandong Li, Karl Meinke, Magnus Myreen, Joseph Near, Virginia Papailiopoulou, Jan Peleska, Dennis Peters, Alexander Pretschner, Antoine Rollet, Kristin Y. Rozier, Andy Schurr, Thomas Sewell, Tomohiko Takagi, Andreas Teucke, T.H. Tse, Mark Utting, Machiel van der Bijl, Luca Viganò, Birgit Vogel-Heuser, TjarkWeber, StephanWeissleder, Tim A.C.Willemse, Christoph Wintersteiger, Burkhart Wolff, Dianxiang Xu, and Steve Zdancewic. Last but not least, the STVR chief editors, Robert Hierons and Jeff Offutt, provided expert guidance and important advice throughout the process.

Modern enterprise systems are often process-based, i.e., they allow for the direct execution of business processes that are specified in a high-level language such as BPMN. In this paper, we present a service, called Security Validation as a Service (SVaaS) for validating the compliance of the business processes during design-time. Basically, while modeling a business process the business analyst specifies as well the security and compliance requirements the business process should comply to. By pressing a button, these requirements are validated and the results are presented in a graphical format to the business analysis. At the core of SVaaS lies a rigorous and industrially viable approach in which the security validation business logic is handled server-side (SVaaS Server) in the Cloud, while the client-side user interface that business analysts use is handled by a light-weight SVaaS Connector. As proof-of-concept we created a SVaaS prototype in which the SVaaS Server is deployed on the SAP NetWeaver Cloud and two SVaaS Connectors are built to enable two well-known BPMN tools, SAP NetWeaver BPM and Activiti, to consume SVaaS against industrial relevant business processes.

Abstract HOL -TestGen is a specification and test case generation environment extending the interactive theorem prover Isabelle/ HOL . As such, Testgen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOL -TestGen method is two-staged: first, the original formula is partitioned into test cases by transformation into a normal form called test theorem . Second, the test cases are analyzed for ground instances (the test data ) satisfying the constraints of the test cases. Particular emphasis is put on the control of explicit test-hypotheses which can be proven over concrete programs. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies.

Modern enterprise systems have to comply to regulations such as Basel III resulting in complex security requirements. These requirements need to be modeled at design-time and enforced at runtime. Moreover, modern enterprise systems are often business-process driven, i.e., the system behavior is described as high-level business processes that are executed by a business process execution engine.

We present a generic modular policy modelling framework and instantiate it with a substantial case study for model-based testing of some key security mechanisms of applications and services of the NPfIT. NPfIT, the National Programme for IT, is a very large-scale development project aiming to modernise the IT infrastructure of the NHS in England. Consisting of heterogeneous and distributed applications, it is an ideal target for model-based testing techniques of a large system exhibiting critical security features.

Collaborations between organizations in the public sector, e.g., fire brigades, polices, military units, is often done via liaison officers. A liaison officer liaises between two organizations by providing a single point of contact and ensuring the efficient communication and coordination of their activities. Usually an organization embeds a liaison officer in another organization to provide face-to-face coordination. Liaison officers demand special requirements to the security mechanism of the IT infrastructure of the organization that act as host for a liaison officer. This holds, in particular, for Disaster Management Information Systems (DMIS). Such systems need, on the one hand, to support various ways of communication in a flexible and ad hoc manner. On the other hand, these systems need to protect, by law, the leakage of sensitive data. In this paper, we present a novel mechanism, based on role-based access control (RBAC), for supporting the flexible and secure information exchange between organizations using liaison officers. Our mechanism enables liaison officers to decide on their own authority which information they wants share with their home organizations while allowing the host organization to limit the access of liaisons officers to their system in a fine-grained manner.

We present an optimization technique for model-based generation of test cases for firewalls. Starting from a formal model for firewall policies in higher-order logic, we derive a collection of semantics-preserving policy transformation rules and an algorithm that optimizes the specification with respect of the number of test cases required for path coverage. The correctness of the rules and the algorithm is established by formal proofs in Isabelle/HOL. Finally, we use the normalized policies to generate test cases with the domain-specific firewall testing tool HOL-TestGen/FW. The resulting procedure is characterized by a gain in efficiency of two orders of magnitude. It can handle configurations with hundreds of rules such as frequently occur in practice. Our approach can be seen as an instance of a methodology to tame inherent state-space explosions in test case generation for security policies.

Access control models are usually static, i.e, permissions are granted based on a policy that only changes seldom. Especially for scenarios in health care and disaster management, a more flexible support of access control, i.e., the underlying policy, is needed.