Memory corruption vulnerabilities have been around for decades and rank among the most prevalent vulnerabilities in embedded systems. Yet this constrained environment poses unique design and implementation challenges that significantly complicate the adoption of common hardening techniques. Combined with the irregular and involved nature of embedded patch management, this results in prolonged vulnerability exposure windows and vulnerabilities that are relatively easy to exploit. Considering the sensitive and critical nature of many embedded systems, this situation merits significant improvement. In this work, we present the first quantitative study of exploit mitigation adoption in 42 embedded operating systems, showing the embedded world to significantly lag behind the general-purpose world. To improve the security of deeply embedded systems, we subsequently present μArmor, an approach to address some of the key gaps identified in our quantitative analysis. μArmor raises the bar for exploitation of embedded memory corruption vulnerabilities, while being adoptable on the short term without incurring prohibitive extra performance or storage costs.

Forensic analysis of malware activity in network environments is a necessary yet very costly and time consuming part of incident response. Vast amounts of data need to be screened, in a very labor-intensive process, looking for signs indicating how the malware at hand behaves inside e.g., a corporate network. We believe that data reduction and visualization techniques can assist security analysts in studying behavioral patterns in network traffic samples (e.g., PCAP). We argue that the discovery of patterns in this traffic can help us to quickly understand how intrusive behavior such as malware activity unfolds and distinguishes itself from the rest of the traffic.In this paper we present a case study of the visual analytics tool EventPad and illustrate how it is used to gain quick insights in the analysis of PCAP traffic using rules, aggregations, and selections. We show the effectiveness of the tool on real-world data sets involving office traffic and ransomware activity.

Programmable Logic Controllers (PLCs) are a family of embedded devices that are being used to control physical processes in critical infrastructures. Similar to other embedded devices, PLCs are vulnerable to memory corruption and control-flow hijacking attacks. Because PLCs are being used for critical control applications, compromised PLCs constitute a significant security and safety risk.

Abstract Trust management is an approach to access control in distributed systems where access decisions are based on policy statements issued by multiple principals and stored in a distributed manner. In trust management, the policy statements of a principal can refer to other principals' statements; thus, the process of evaluating an access request (i.e., a goal) consists of finding a “chain” of policy statements that allows the access to the requested resource. Most existing goal evaluation algorithms for trust management either rely on a centralized evaluation strategy, which consists of collecting all the relevant policy statements in a single location (and therefore they do not guarantee the confidentiality of intensional policies), or do not detect the termination of the computation (i.e., when all the answers of a goal are computed). In this paper, we present GEM, a distributed goal evaluation algorithm for trust management systems that relies on function-free logic programming for the specification of policy statements. GEM detects termination in a completely distributed way without disclosing intensional policies, thereby preserving their confidentiality. We demonstrate that the algorithm terminates and is sound and complete with respect to the standard semantics for logic programs.

Systems of systems (SoS) are dynamic coalitions of distributed, autonomous and heterogeneous systems that collaborate to achieve a common goal. While offering several advantages in terms of scalability and flexibility, the SoS paradigm has a strong impact on systems interoperability and on the security requirements of the collaborating parties. In this paper, we introduce a service-oriented security framework that protects the information exchanged among the parties in an SoS, while preserving parties' autonomy and interoperability. Confidentiality and integrity of information are protected by combining context-aware access control with trust management. Autonomy and interoperability among parties are enabled by the use of ontology-based services. More precisely, parties may refer to different ontologies to define the semantics of the terms used in their security policies and to describe domain knowledge and context information; a semantic alignment technique is then employed to map concepts from different ontologies and align the parties' vocabularies. We demonstrate the applicability of our solution by deploying a prototype implementation of the framework in an SoS in the maritime safety and security domain.

There are different paradigms for enforcing information flow and declassification policies. These approaches can be divided into static analyzers and runtime enforcers. Each class has its own strengths and weaknesses, each being able to enforce a different set of policies. In this paper, we introduce a hybrid static-runtime enforcement mechanism that works on unannotated program code and supports information-flow control, as well as declassification policies. Our approach manages to enforce realistic policies, as shown by our three running examples, all within the context of a mobile device application, which cannot be handled separately by static or runtime approaches, and are also not covered by current access control models of mobile platforms such as Android or iOS. We also show that including an intermediate step (called preload check) makes both the static analysis system independent (in terms of security labels) and the runtime enforcer lightweight. Finally, we implement our runtime enforcer and run experiments that show that its overhead is so low that the approach can be rolled out on current mobile systems.

For today’s organisations, having a reliable information system is crucial to safeguard enterprise revenues (think of on-line banking, reservations for e-tickets etc.). Such a system must often offer high guarantees in terms of its availability; in other words, to guarantee business continuity, IT systems can afford very little downtime. Unfortunately, making an assessment of IT availability risks is difficult: incidents affecting the availability of a marginal component of the system may propagate in unexpected ways to other more essential components that functionally depend on them. General-purpose risk assessment (RA) methods do not provide technical solutions to deal with this problem. In this paper we present the qualitative time dependency (QualTD) model and technique, which is meant to be employed together with standard RA methods for the qualitative assessment of availability risks based on the propagation of availability incidents in an IT architecture. The QualTD model is based on our previous quantitative time dependency (TD) model (Zambon et al. in BDIM ’07: Second IEEE/IFIP international workshop on business-driven IT management. IEEE Computer Society Press, pp 75–83, 2007), but provides more flexible modelling capabilities for the target of assessment. Furthermore, the previous model required quantitative data which is often too costly to acquire, whereas QualTD applies only qualitative scales, making it more applicable to industrial practice. We validate our model and technique in a real-world case by performing a risk assessment on the authentication and authorisation system of a large multinational company and by evaluating the results with respect to the goals of the stakeholders of the system. We also perform a review of the most popular standard RA methods and discuss which type of method can be combined with our technique.

CRAC is an IT-infrastructure-based method for assessing and comparing confidentiality risks of distributed IT systems. The method determines confidentiality risks by taking into account the effects of the leakage of confidential information (e.g. industrial secrets), and the paths that may be followed by different attackers (e.g. insider and outsider). We evaluate its effectiveness by applying it to a real-world outsourcing case.

Simple non-interference is too restrictive for specifying and enforcing information flow policies in most programs. Exceptions to non-interference are provided using declassification policies. Several approaches for enforcing declassification have been proposed in the literature. In most of these approaches, the declassification policies are embedded in the program itself or heavily tied to the variables in the program being analyzed, thereby providing little separation between the code and the policy. Consequently, the previous approaches essentially require that the code be trusted, since to trust that the correct policy is being enforced, we need to trust the source code. In this paper, we propose a novel framework in which declassification policies are related to the source code being analyzed via its I/O channels. The framework supports many of the of declassification policies identified in the literature. Based on flow-based static analysis, it represents a first step towards a new approach that can be applied to untrusted and legacy source code to automatically verify that the analyzed program complies with the specified declassification policies. The analysis works by constructing a conservative approximation of expressions over input channel values that could be output by the program, and by determining whether all such expressions satisfy the declassification requirements stated in the policy. We introduce a representation of such expressions that resembles tree automata. We prove that if a program is considered safe according to our analysis then it satisfies a property we call Policy Controlled Release, which formalizes information-flow correctness according to our notion of declassification policy. We demonstrate, through examples, that our approach works for several interesting and useful declassification policies, including one involving declassification of the average of several confidential values.

We introduce the use, monitoring, and enforcement of integrity constraints in trust management-style authorization systems. We consider what portions of the policy state must be monitored to detect violations of integrity constraints. Then, we address the fact that not all participants in a trust-management system can be trusted to assist in such monitoring, and show how many integrity constraints can be monitored in a conservative manner so that trusted participants detect and report if the system enters a policy state from which evolution in unmonitored portions of the policy could lead to a constraint violation.

Large and distributed access control systems are increasingly common, for example in health care. In such settings, access control policies may become very complex, thus complicating correct and efficient adminstration of the access control system. Despite being one of the most widely used access control standards, RBAC does not include an administration model for distributed systems. In this paper we fill this gap. We present a model for the administration of RBAC in a distributed system and propose an administration procedure supporting the principle that different systems protect different sets of objects. We demonstrate that our procedure fulfills the formal requirements deriving from safety and availability, and we show how it can be translated to a practical implementation. Finally, we show how our model can be extended with multiple decentralized administrative systems.

In existing RBAC literature, administrative privileges are inherited just like ordinary user privileges. We argue that from a security viewpoint this is too restrictive, and we believe that a more flexible approach can be very useful in practice. We define an ordering on the set of administrative privileges, enabling us to extend the standard privilege inheritance relation in a natural way. This means that if a user has a particular administrative privilege, then she is also implicitly authorized for weaker administrative privileges. We prove the non-trivial result that it is possible to decide whether one administrative privilege is weaker than another and show how this result can be used to decide administrative requests in an RBAC security monitor.

While preventative policy enforcement mechanisms can provide theoretical guarantees that policy is correctly enforced, they have limitations in practice. They are inflexible when unanticipated circumstances arise, and most are either inflexible with respect to the policies they can enforce or incapable of continuing to enforce policies on data objects as they move from one system to another. In this paper we propose an approach to enforcing policies not by preventing unauthorized use, but rather by deterring it. We believe this approach is complementary to preventative policy enforcement. We call our approach APPLE for A-Posteriori PoLicy Enforcement. We introduce APPLE Core, a logical framework for using logs to verify that actions taken by the system were authorized. A trust management system is used to ensure that data objects are provided only to users operating on auditable systems who are subject to penalty should they be found in violation. This combination of audit and accountability provides a deterence that strongly encourages trustworthy behavior, thereby allowing a high level of assurance of end-to-end policy enforcement.

We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol, where timing information allows the study of differ

We propose VS-LTL, a pure-past security linear temporal logic that allows the specification of a variety of authentication, secrecy and data freshness properties. Furthermore, we present a sound and complete decision procedure to establish the validity of security properties for symbolic execution traces, and show the integration with constraint-based analysis techniques

This special issue is inspired by the homonymous ICLP workshops that took place during ICLP 2001 and ICLP 2002. Extending and shifting slightly from the scope of their predecessors (on verification and logic languages) held in the context of previous editions of ICLP, the aim of the SAVE workshops was to bring together researchers interested in the use of computational logic as a tool for the specification, the analysis and the validation of systems, with particular emphasis on emerging technologies such as World Wide Web and E-Commerce, (protocols for) Smart Cards and Mobile Telephony, Wireless Technology, Hybrid Systems, Real-Time and Distributed systems, etc.

We introduce the use, monitoring, and enforcement of integrity constraints in trust management-style authorization systems. We consider what portions of the policy state must be monitored to detect violations of integrity constraints. Then we address the fact that not all participants in a trust management system can be trusted to assist in such monitoring, and show how many integrity constraints can be monitored in a conservative manner so that trusted participants detect and report if the system enters a policy state from which evolution in unmonitored portions of the policy could lead to a constraint violation.

In logic programming,dynamic schedulingindicates the feature by means of which the choice of the atom to be selected at each resolution step is done at runtime and does not follow a fixed selection rule such as the left-to-right one of Prolog.Input-consuming derivationswere introduced to model dynamic scheduling while abstracting from the technical details. In this article, we provide a sufficient and necessary criterion for termination of input-consuming derivations of simply moded logic programs. The termination criterion we propose is based on a denotational semantics for partial derivations which is defined in the spirit of model-theoretic semantics previously proposed for left-to-right derivations.

We propose a modular method for proving termination of general logic programs (i.e. logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider programs consisting of a hierarchy of modules and supply a general result for proving termination by dealing with each module separately. For programs which are in a certain sense well-behaved, namely well-moded or well-typed programs, we derive both a simple verification technique and an iterative proof method. Some examples show how our system allows for greatly simplified proofs.

We study the properties of input-consuming derivations of moded logic programs. Input-consuming derivations can be used to model the behavior of logic programs using dynamic scheduling and employing constructs such as delay declarations. We consider the class of nicely-moded programs and queries. We show that for these programs a weak version of the well-known switching lemma holds also for input-consuming derivations. Furthermore, we show that, under suitable conditions, there exists an algebraic characterization of termination of input-consuming derivations.

We introduce a transformation system for concurrent constraint programming (CCP). We define suitable applicability conditions for the transformations that guarantee the input/output CCP semantics is also preserved when distinguishing deadlocked computations from successful ones and when considering intermediate results of (possibly) nonterminating computations.The system allows us to optimize CCP programs while preserving their intended meaning: In addition to the usual benefits for sequential declarative languages, the transformation of concurrent programs can also lead to the elimination of communication channels and of synchronization points, to the transformation of nondeterministic computations into deterministic ones, and to the crucial saving of computational space. Furthermore, since the transformation system preserves the deadlock behavior of programs, it can be used for proving deadlock-freeness of a given program with respect to a class of queries. To this aim, it is sometimes sufficient to apply our transformations and to specialize the resulting program with respect to the given queries in such a way that the obtained program is trivially deadlock-free.

The problem of partitioning grid-based applications for parallel computing can be solved easily and intuitively in a logic programming language such as Prolog, using only the single assignment property of the logic variable, and not the backtracking. We show that such a logic program can be transformed in a systematic way into a circular functional program, which runs 10 times faster than the original logic program. The transformation proceeds in a number of steps. The first step is novel, and we give a correctness proof. Our reasoning also uses a novel combination of concepts from both the logical and functional paradigms. Copyright © 1999 John Wiley & Sons, Ltd.

In this paper we study unfold/fold transformations for constraint logic programs (CLP) with dynamic scheduling and for concurrent constraint programming (CCP). We define suitable applicability conditions for these transformations which guarantee that the original and the transformed program have the same results of successful derivations and the same deadlock free queries.The possible applications of these results are twofold. On one hand we can use the unfold/fold system to optimize CLP and CCP programs while preserving their intended meaning and in particular without the risk of introducing deadlocks. On the other hand, unfold/fold transformations can be used for proving deadlock freeness of a class of queries in a given program: to this aim it is sufficient to apply our transformations and to specialize the resulting program with respect to the given queries in such a way that the obtained program is trivially deadlock free. As shown by several interesting examples, this yields a methodology for proving deadlock freeness which is simple and powerful at the same time.

The simultaneous replacement transformation operation is here defined and studied w.r.t. normal programs. We give applicability conditions able to ensure the correctness of the operation w.r.t. the set of logical consequences of the completed database. We consider separately the cases in which the underlying language is infinite and finite; in this latter case we also distinguish according to the kind of domain closure axioms adopted. As corollaries we obtain results for Fitting's and Kunen's semantics. We also show how simultaneous replacement can mimic other transformation operations such as thinning, fattening and folding, thus producing applicability conditions for them too.

In this paper we study the replacement transformation for Constraint Logic Programming modules. We define new applicabihty conditions which guarantee the correctness of the operation also wrt module¿s composition: under this conditions, the original and the transformed modules have the same observable properties also when they are composed with other modules. Furthermore, the applicability y conditions are uot bound to a specific notion of observable. Here we consider three distinct such notions: two of them are operational and are based on the computed constraints; the third one is the algebraic one based on the least model. We show that our transformation method can be applied in any of these distinct contexts, thus providing a parametric approach.

An unfold/fold transformation system is a source-to-source rewriting methodology devised to improve the efficiency of a program. Any such transformation should preserve the main properties of the initial program: among them, termination. In the field of logic programming, the class of acyclic programs plays an important role in this respect, since it is closely related to the one of terminating programs. The two classes coincide when negation is not allowed in the bodies of the clauses. We prove that the Unfold/Fold transformation system defined by Tamaki and Sato preserves the acyclicity of the initial program. From this result, it follows that when the transformation is applied to an acyclic program, then the finite failure set for definite programs is preserved; in the case of normal programs, all major declarative and operational semantics are preserved as well. These results cannot be extended to the class of left-terminating programs without modifying the definition of the transformation.