Biblio

Heterogeneous system-on-chip platforms with multiple processing cores are becoming increasingly common in safety-and security-critical embedded systems. To facilitate a logical isolation of physically connected on-chip components, internal communication links of such platforms are often equipped with dedicated access protection units. When performed manually, however, the configuration of these units can be both time-consuming and error-prone. To resolve this issue, we present a formal model and a corresponding design methodology that allows developers to specify access permissions and information flow requirements for embedded systems in a mostly platform-independent manner. As part of the methodology, the consistency between the permissions and the requirements is automatically verified and an extensible generation framework is used to transform the abstract permission declarations into configuration code for individual access protection units. We present a prototypical implementation of this approach and validate it by generating configuration code for the access protection unit of a commercially available multiprocessor system-on-chip.

Hypergame theory has been used to model advantages in decision making. This research provides a formal representation of deception to further extend the hypergame model. In order to extend the model, we propose a hypergame theoretic framework based on temporal logic to model decision making under the potential for trust and deception. Using the temporal hypergame model, the concept of trust is defined within the constraints of the model. With a formal definition of trust in hypergame theory, the concepts of distrust, mistrust, misperception, and deception are then constructed. These formal definitions are then applied to an Attacker-Defender hypergame to show how the deception within the game can be formally modeled; the model is presented. This demonstrates how hypergame theory can be used to model trust, mistrust, misperception, and deception using a formal model.

The supervisory control and data acquisition (SCADA) network in a smart grid requires to be reliable and efficient to transmit real-time data to the controller. Introducing SDN into a SCADA network helps in deploying novel grid control operations, as well as, their management. As the overall network cannot be transformed to have only SDN-enabled devices overnight because of budget constraints, a systematic deployment methodology is needed. In this work, we present a framework, named SDNSynth, that can design a hybrid network consisting of both legacy forwarding devices and programmable SDN-enabled switches. The design satisfies the resiliency requirements of the SCADA network, which are specified with respect to a set of identified threat vectors. The deployment plan primarily includes the best placements of the SDN-enabled switches. The plan may include one or more links to be installed newly. We model and implement the SDNSynth framework that includes the satisfaction of several requirements and constraints involved in resilient operation of the SCADA. It uses satisfiability modulo theories (SMT) for encoding the synthesis model and solving it. We demonstrate SDNSynth on a case study and evaluate its performance on different synthetic SCADA systems.

Often, analysts have to face a challenging situation when formally verifying the implementation of a security protocol: they need to build a model of the protocol from only poorly or not documented code, and with little or no help from the developers to better understand it. Security protocols implementations frequently use services provided by libraries coded in the C programming language; automatic tools for codelevel reverse engineering offer good support to comprehend the behavior of code in object-oriented languages but are ineffective to deal with libraries in C. Here we propose a systematic, yet human-dependent approach, which combines the capabilities of state-of-the-art tools in order to help the analyst to retrieve, step by step, the security protocol specifications from a library in C. Those specifications can then be used to create the formal model needed to carry out the analysis.

While the control of individuals over their personal data is increasingly seen as an essential component of their privacy, the word "control" is usually used in a very vague way, both by lawyers and by computer scientists. This lack of precision may lead to misunderstandings and makes it difficult to check compliance. To address this issue, we propose a formal framework based on capacities to specify the notion of control over personal data and to reason about control properties. We illustrate our framework with social network systems and show that it makes it possible to characterize the types of control over personal data that they provide to their users and to compare them in a rigorous way.

Two emerging architectural paradigms, i.e., Software Defined Networking (SDN) and Network Function Virtualization (NFV), enable the deployment and management of Service Function Chains (SFCs). A SFC is an ordered sequence of abstract Service Functions (SFs), e.g., firewalls, VPN-gateways, traffic monitors, that packets have to traverse in the route from source to destination. While this appealing solution offers significant advantages in terms of flexibility, it also introduces new challenges such as the correct configuration and ordering of SFs in the chain to satisfy overall security requirements. This paper presents a formal model conceived to enable the verification of correct policy enforcements in SFCs. Software tools based on the model can then be designed to cope with unwanted network behaviors (e.g., security flaws) deriving from incorrect interactions of SFs of the same SFC. 

Formal methods, models and tools for social big data analytics are largely limited to graph theoretical approaches such as social network analysis (SNA) informed by relational sociology. There are no other unified modeling approaches to social big data that integrate the conceptual, formal and software realms. In this paper, we first present and discuss a theory and conceptual model of social data. Second, we outline a formal model based on set theory and discuss the semantics of the formal model with a real-world social data example from Facebook. Third, we briefly present and discuss the Social Data Analytics Tool (SODATO) that realizes the conceptual model in software and provisions social data analysis based on the conceptual and formal models. Fourth and last, based on the formal model and sentiment analysis of text, we present a method for profiling of artifacts and actors and apply this technique to the data analysis of big social data collected from Facebook page of the fast fashion company, H&M.