SCSS 2017: Papers with Abstracts

Abstract. In previous work we presented an algorithmic procedure for analysing the space complexity of monitor specifications written in a fragment of predicate logic. These monitor specifications were developed for runtime monitoring of event streams. Our procedure provides accurate results for a large fragment of the possible specifications, but overestimates the space complexity of precisely those specifications which are more likely to be found in real world applications. Experiments hinted at a relationship between the extent our procedure over-approximates the space requirements of a specification and the quantifier structure of the specification. In this paper we provide a formalization of this relationship as approximation ratios, and are able to pinpoint ``good'' constructions, that is specifications using less memory. These results are first steps towards categorizing specifications based on memory efficiency.

Abstract. We provide a new technique for pattern matching that is based on components for each match. The set of match statements and their order is open for configuration at the right time and takes place in a feature-oriented fashion. This gives rise to a solution to the Expression Problem in presence of defaults. It takes a lightweight discipline to develop components for our technique. Their use for configuration of the pattern match, however, is virtually automatic.

Abstract. We introduce a logic called C2PDLS, motivated by some reasoning
about graph rewriting systems. C2PDLS is an extension of both
combinatory propositional dynamic logic, usually written CPDL,
and converse propositional dynamic logic, usually written CPDL
too. In addition to the existing features of both CPDLs, the
introduced logic offers the possibility to use the notion of
substitutions à la Hoare within its formulae. Such substitutions
reflect the effect of some actions on graph structures such as
addition or deletion of edges or nodes. These last features led
us to introduce restricted universal roles over subsets of the
universe. We propose a sound and complete deductive system for
C2PDLS and show that its validity problem is decidable.

Abstract. Conformance testing is an operational way of determining whether an implementation conforms to the specification or not. It has a rich underlying theory wherein the specification and the implemen- tation under test (IUT) are each modeled by a timed automaton with inputs and outputs (TAIO), a variant of the classical timed automaton [1]. Test cases generated from the specification TAIO are symbolically executed against the implementation TAIO. Depending upon how test cases interact with the IUT, testing can be synchronous or asynchronous. In synchronous testing a test case interacts with the IUT directly, whereas in asynchronous testing a test case interacts with the IUT through a pair of first-in-first-out (FIFO) channels. Different approaches for synchronous testing of real-time systems have already been proposed [5],[7],[4],[8]. In this paper we propose an approach which is aimed at testing real-time systems asynchronously (i.e., remotely through some medium)

Abstract. We present two techniques for transforming any prefix-constrained and any controlled term rewrite system into an ordinary rewrite system. We prove that both transformations preserve the rewrite com- putations, and preserve termination. In this way, prefix-constrained rewriting and controlled rewriting can be run, and termination can be checked, using the usual tools for ordinary rewriting.

Abstract. Interacting with geographically proximate users who present similar interests and preferences is a key service offered by mobile social networks which leads to the creation of new connections that combine physical and social closeness. Usually these interactions are based on social profile matching where users publish their preferences and attributes to enable the search for a similar profile. Such public search would result in the leakage of sensitive or identifiable information to strangers who are not always potential friends. As a consequence this promising feature of mobile social networking may cause serious privacy breaches if not addressed properly. Most existent work relies on homomorphic encryption for privacy preservation during profile matching, while we propose in this paper a novel approach based on the fuzzy extractor which performs private matching of two sets and reveals them only if they overlap considerably. Our scheme achieves a desirable trade off between security and complexity.

Abstract. Firewall has been at the center of intense research in the last decade owing to the increase of malicious attacks on networks. Constant updating of the firewall configuration by modifying, adding and removing rules increases the complexity of the configuration resulting in overlapping and often conflicting filtering rules. As a consequence, the set of filtering rules becomes unreliable and contains multiple misconfigurations creating ambiguity in classification of new traffic, not only affecting the performance of the firewall, but also putting the system in a vulnerable position. Manual management of this problem can be overwhelming and potentially inaccurate. Therefore, there is a need of automated methods to analyze, detect and fix misconfigurations. The objective of our work is to propose (1) a new formal approach to discover effective firewall configurations errors, (2) an optimal and automatic method with the minimum number of operations to correct these misconfigurations in both centralized firewalls and firewalls in a distributed environment and (3) a tool that implements proposed techniques and significantly helps user in discovering and resolving firewall misconfigurations.

Abstract. The constant evolution of access control requirements and the dynamic environment in which they evolve require nowadays quick and instant decision-making related to risk of illegitimate access in Information Systems. Various contributions defined in the literature aim to overcome or to mitigate related risks and paradoxically adopted the hypothesis of reliability and validity of access control policies. However, the corruption of these policies is a security aspect of great importance and should be handled actively because (i) an access control policy is also exposed to the same threats as the managed data is and (ii) properties and parameters of the concrete policy at a given stage may differ, in a critical manner, from a reference stage. We define a reliable and complete solution for risk management in the context of Database Servers. We intend to define a rigorous risk management approach that mainly verifies recommendations of the standard ISO 31000:2009. Our approach takes into consideration all identified threats on a Database Server and provides an environment for the analysis of the correlation
between the threats detected in particular by different security devices.
To ensure a high level of surety, we opt for defining a formal framework that allows to efficiently address this problematic and to formally represent and verify our risk management
processes.

Abstract. We present a generalization of mathematical origami to higher dimensions. We briefly explain Huzita- Justin’s axiomatic treatment of mathematical origami. Then, for concreteness, we apply it to origami on 3-dimensional Euclidean space in which the fold operation consists of selecting a half-plane and reflect- ing one half-plane across it. We finally revisit the subject from an n-dimensional point of view.

Abstract. The enumeration problem addresses a collection of important algorithmic issues related to distributed computations. Among existing solutions, we are interested on the seminal algorithm of Mazurkiewicz, based on local computations. Our paper contributes to the design of a correct-by-construction enumeration algorithm. The main idea relies upon the development of the problem following a top/down approach
that can be supported by an incremental process controlled by the refinement of models. Event-B modelling language is supporting our methodological. Our main objective is to provide a verified component for distributed enumeration in
order to be used and extended for solving other problems of distributed algorithms.

Abstract. Model checking is a powerful and widespread technique for the verification of finite dis- tributed systems. It takes as input a formal model of a system and a formal specification (formula) of a property to be checked, and states whether the system satisfies the property or not. Since it is based on state space traversal algorithms, the model checking approach suffers from the well known state space explosion problem. Indeed the space (and conse- quently the time) requirements increase exponentially with the size of the models. One way to deal with this problem is symbolic model checking. It aims at checking the prop- erty on a compact representation of the system by using Binary Decision Diagram (BDD) techniques. Another way is to parallelize the construction/traversal of the state space on multiple processors. In this paper, we combine the two mentioned approaches by propos- ing an efficient multi-threaded algorithm for the construction of the so called Symbolic Observation Graph (SOG). It is a hybrid structure where the transitions of the system are divided into observed and unobserved ones. The nodes of this graph are then defined as sets of states linked with unobserved transitions (and encoded symbolically with a BDD) and edges are labeled with observed transitions only (and represented explicitly). The basic idea is that each thread owns one part of the SOG construction. We measured the runtime of the parallel SOG construction algorithm on several models, and the obtained results are very competitive. The preliminary evaluations we have done on standard examples show that our method outperforms the sequential method which makes it attractive.

Abstract. Nowadays, the access control is becoming increasingly important for open, ubiquitous and criti- cal systems. Nonetheless, efficient Administration, Management, Safety analysis and Risk assessment (AMSR) are recognized as fundamental and crucial challenges in todays access control infrastructures. In untrustworthy environment, the administration of an access control policy, which is a main secu- rity aspect, generally raises a critical analysis problem when the administration is distributed and/or potentially un-trusted users contribute to this process. Consequently, collusions attempts and inner threats may take place to generate crucial and invisible breaches to circumvent the policy. To address this issue, we introduce a rigorous and comprehensive solution for an efficient and secure management of access control policies. Our proposal gives a high visibility on the development process of an access control policy and allows in an elegant manner to detect, analyze and assess the risk associated to the policy defects. The strength of our proposal is that it relies on logic-like formalisms to ensure a high surety by verifying the correctness and the completeness of our formal reasoning. We rely on an example to illustrate the relevance of the proposal.