The use of security patterns has been recognized as effective in mitigating vulnerabilities in software systems. However, it is still not well understood how they can be applied systematically and effectively in concrete systems to achieve the best results. We present a formal approach based on the Alloy model checker to detect information disclosure vulnerabilities and enforce appropriate security patterns automatically. The approach helps improve the overall security posture of software systems while reducing the dependence on manual security analysis. We demonstrate the usability of our approach through the use case of a Smart Meter Gateway. The proposed approach is generic and constitutes a significant advancement toward systematic methods for designing secure software systems.

The specification and the verification of security requirements is one of the major computer-based systems challenges. Security requirements need to be precisely specified before a tool can manipulate them, and though several approaches to security requirements specification have been proposed, they do not provide the scalability and flexibility required in practice. We take this problem towards an integrated approach for security requirement specification and treatment during the software architecture design time. The general idea of the approach is to: (1) specify security requirements as properties of a modeled system in a technology-independent specification language; (2) implement the developed model in a suitable language with tool support for requirement satisfaction through model verification; and (3) suggest a set of security policies to constrain the operation of the system and to guarantee the security properties. In the scope of this paper, we use first-order logic as a formalism that is abstract and technology-independent and Alloy as a tooled language used in modeling and software development. To validate our work, we explore a set of representative security properties from categories based on CIA classification in the context of secure component-based software architecture development.

This work is devoted to the problem of spanning trees maintenance in the presence of crash failures in a distributed environment using only local knowledge. Using a pre-constructed spanning tree of a k-connected graph, we present a protocol to maintain a spanning tree in the presence of k-1 consecutive failures. The contribution of this paper is threefold. First, the problem is formalized as an occurrence of Menger's theorem in a distributed setting. The second result shows an implementation of the protocol which is composed of a set of modules encoded using a graph relabeling systems model. The last contribution is the implementation of this protocol in the asynchronous message passing model. For a given graph G =(V,E), where M is the number of its edges, N is the number of its nodes, and Δ is its degree; After each failure occurrence, our algorithms need the following requirements: The first one uses O(Δ × N) steps and O(Δ) bits per node. The second one uses O(N+M) messages and O(N) time and O(Δ) bits per node. In addition, we investigate the possible specification and verification of the presented algorithm using Alloy as a tooled formal language.