Attack trees are a popular notation for describing threats to systems, both in academia and industry. Originally, attack trees lacked a formal semantics, but formal semantics for different variants of attack trees were proposed later. These semantics focus on the attacker's actions defined in the leaves and the logical structure defined by the inner nodes of an attack tree. Surprisingly, they do not clarify the connection to the goal defined at the root node in a satisfactory fashion. In this article, we aim at a better clarification of this connection between the attacks and the attacker goal specified by an attack tree. We argue that there are multiple sensible success criteria for attacks wrt. a given attacker goal and develop a framework for defining such criteria. We exploit our framework to identify similarities and differences between automatic attack-tree generation techniques. Finally, we propose a novel variant of attack trees that allows one to express exploits in an explicit fashion.

The medical industry is increasingly digitalized and Internet-connected (e.g., Internet of Medical Things), and when deployed in an Internet of Medical Things environment, software-defined networks (SDNs) allow the decoupling of network control from the data plane. There is no debate among security experts that the security of Internet-enabled medical devices is crucial, and an ongoing threat vector is insider attacks. In this paper, we focus on the identification of insider attacks in healthcare SDNs. Specifically, we survey stakeholders from 12 healthcare organizations (i.e., two hospitals and two clinics in Hong Kong, two hospitals and two clinics in Singapore, and two hospitals and two clinics in China). Based on the survey findings, we develop a trust-based approach based on Bayesian inference to figure out malicious devices in a healthcare environment. Experimental results in either a simulated and a real-world network environment demonstrate the feasibility and effectiveness of our proposed approach regarding the detection of malicious healthcare devices, i.e., our approach could decrease the trust values of malicious devices faster than similar approaches.

One of the big problems of risk assessment in information security is the quantification of risk-related properties, such as vulnerability. Vulnerability expresses the likelihood that a threat agent acting against an asset will cause impact, for example, the likelihood that an attacker will be able to crack a password or break into a system. This likelihood depends on the capabilities of the threat agent and the strength of the controls in place. In this paper, we provide a framework for estimating these three variables based on the Elo rating used for chess players. This framework re-interprets security from the field of Item Response Theory. By observing the success of threat agents against assets, one can rate the strength of threats and controls, and predict the vulnerability of systems to particular threats. The application of Item Response Theory to the field of risk is new, but analogous to its application to children solving math problems. It provides an innovative and sound way to quantify vulnerability in models of (information) security.

Networked communication systems and the data they make available have, over the last decades, made their way to the very core of both society and business. Not only do they support everyday life and day-to-day operations, in many cases they enable them in the first place, and often are among the most valuable assets. The flexibility that makes them so valuable in the first place, is also their primary vulnerability: via the network, an entity's data is accessible from almost everywhere, often without the need of physical presence in the entity's perimeter. In this work we propose a new security paradigm, that aims at using the network's flexibility to move data and applications away from potential attackers. We also present a possible realization of the proposed paradigm, based on recent advances in language-based security and static analysis, where data and applications are partitioned ahead-of-time and can be moved automatically based on activity both in the network as well as the real world.

Policy conformance is a security property gaining importance due to commercial interest like Digital Rights Management. It is well known that static analysis can be used to validate a number of more classical security policies, such as discretionary and mandatory access control policies, as well as communication protocols using symmetric and asymmetric cryptography. In this work we show how to develop a Flow Logic for validating the conformance of client software with respect to a licence conformance policy. Our approach is sufficiently flexible that it extends to fully open systems that can admit new services on the fly.

Java Virtual Machines (JVMs) traditionally perform bytecode verification by way of an iterative dataflow analysis. Bytecode verification is necessary to ensure type safety because temporary variables in the JVM are not statically typed. We present an alternative verification mechanism that transforms JVM bytecode into Static Single Assignment Form (SSA) and thereby propagates definitions directly to uses. Type checking at control flow merge points can then be performed in a single pass. Our prototype implementation of the new algorithm is faster than the standard JVM bytecode verifier. It has the additional benefit of generating SSA as a side effect, which may be immediately useful for a subsequent dynamic compilation stage.

The /spl mu/Klaim calculus is a process algebra designed to study the programming of distributed systems consisting of a number of locations each having their own tuple space and collection of mobile processes. Previous work has explored how to incorporate a notion of capabilities to be enforced dynamically by means of a reference monitor. Our first contribution is to describe a sandboxing semantics for the remote evaluation of mobile code; we then develop a succinct flow logic for statically guaranteeing the properties enforced by the reference monitor and hence for dispensing with the overhead of a dynamic reference monitor. Our second contribution is an extension of the calculus to interact with an environment; processes enter the system from the environment and we develop an entry-condition that is sufficient for ensuring that the resulting system continues to guarantee the properties that would otherwise need to be dynamically enforced by the reference monitor. We call the resulting calculus myKlaim.

The coordination of layers in computer and software systems is one of the main challenges in designing such systems today. In this paper we consider Holistic System Design as a way of integrating requirements and facilities of different system layers. We also discuss some of the challenges that this kind of system design poses for computer science in general as well as programming languages and operating systems in particular.

This report gives an overview over the Workshop on Programming Languages and Operating Systems (PLOS 2006), which was colocated with ASPLOS XII. It introduces the motivation for the work-shop and gives a summary of the workshop contributions.

We present a just-in-time compiler for a Java VM that is small enough to fit on resource-constrained devices, yet is surprisingly effective. Our system dynamically identifies traces of frequently executed bytecode instructions (which may span several basic blocks across several methods) and compiles them via Static Single Assignment (SSA) construction. Our novel use of SSA form in this context allows to hoist instructions across trace side-exits without necessitating expensive compensation code in off-trace paths. The overall memory consumption (code and data) of our system is only 150 kBytes, yet benchmarks show a speedup that in some cases rivals heavy-weight just-in-time compilers.

We predict that we will soon witness attacks on all kinds of systems that will be based on the attacked systems' worst-case behavior. For example, the worst-case performance of Java Bytecode Verification rises quadratically with program length. By sending a legal, but difficult-to-verify program to a server virtual machine, we can keep that server occupied for an inordinate amount of time, effectively making it unavailable for useful work. The problem, however, is not restricted to mobile-code verification: for example, an attacker could exploit knowledge about a just-in-time compiler's register allocator by sending it a particularly difficult to solve graph-coloring puzzle. The same vulnerability can be exploited if the attacker has intimate knowledge of the data structures used in the attacked system. Similar problems occur in hardware, e.g. with respect to power variability or the heat dissipation of processors. Malicious programs can exploit which parts of computer chips dissipate power, thereby overheating regions of the chip that are known to contain no temperature sensors. This attack could be used to affect battery life or cause early chip aging. Unfortunately, worst case-based attacks are hard to counter without also limiting the system's behavior in the average case.