Search

When peers rate each other, they may rate inaccurately to boost their own reputation or unfairly lower another’s. This could be mitigated by having a reputation server incentivise accurate ratings with a reward. However, assigning rewards becomes challenging when ratings are anonymous, since the reputation server cannot tell which peers to reward for rating accurately. To address this, we propose an anonymous peer rating system in which users can be rewarded for accurate ratings, and we formally define its model and security requirements. In our system ratings are rewarded in batches, so that users claiming their rewards only reveal they authored one in this batch of ratings. To ensure the anonymity set of rewarded users is not reduced, we also split the reputation server into two entities, the Rewarder, who knows which ratings are rewarded, and the Reputation Holder, who knows which users were rewarded. We give a provably secure construction satisfying all the security properties required. For our construction we use a modification of a Direct Anonymous Attestation scheme to ensure that peers can prove their own reputation when rating others, and that multiple feedback on the same subject can be detected. We then use Linkable Ring Signatures to enable peers to be rewarded for their accurate ratings, while still ensuring that ratings are anonymous. Our work results in a system which allows accurate ratings to be rewarded, whilst still providing anonymity of ratings with respect to the central entities managing the system.

Dissertação de mestrado integrado em Informatics Engineering, Industrial manufacturing is becoming highly reliant on automation developments, as they bring more efficient and accurate processes, with lower associated costs. Consequently, robots are increasingly being deployed in a wide range of scenarios, especially where safety is demanded. In such cases, it is critical to employ appropriate procedures to verify both the system’s quality and safety. Following the current growth of cyber-physical systems, as well as their usage in various technology domains, the development of software applications is becoming more demanding due to the complexity behind the integration of complementing services, beyond those provided by the operating system. One of the most popular open-source software platforms for building robotic systems is the Robot Operating System (ROS) [53] middleware, where highly configurable robots are usually built by composing third-party modules. Robot Operating System 2 (ROS2) is implemented using the Data Distribution Service (DDS) [49] communication protocol. ROS2 implicitly makes use of the DDS-Security artefacts through the Secure Robot Operating System 2 (SROS2) security toolset. The present study focus on detecting security problems in ROS2 networks, in which it is intended to verify, through formal techniques, security properties. However, security is a very broad subject, so this study focuses on a particular security property to show the viability of the proposed technique, namely Observational Determinism (OD). This dissertation introduces a software tool, named Security Verification in ROS (svROS), that provides multiple functionalities to support this type of security analysis using Alloy [32], a formal specification language and analysis tool., A crescente implementação de processos automáticos tem motivado a reestruturação nos mais diversos setores industriais, com o objetivo de aumentar a eficiência e precisão dos mesmos, e consequentemente, reduzir os custos associados. Além disso, esta ideia levou à integração da robótica nos mais amplos domínios tecnológicos, especialmente onde a segurança é exigida. Nestes casos, é fundamental adotar técnicas apropriadas de forma a verificar tanto a qualidade do sistema, como a segurança do mesmo. Como resultado do atual crescimento dos sistemas ciber-físicos, nomeadamente sistemas robóticos, bem como a sua utilização em vários domínios tecnológicos, o desenvolvimento de aplicações tem vindo a ficar mais exigente, em particular devido à complexidade da integração dos serviços necessários, tipicamente não fornecidos pelo sistema operativo. Uma das plataformas considerada como standard no que toca ao desenvolvimento de sistemas robóticos é o middleware ROS [53], onde robôs altamente configuráveis são construídos através da composição modular de software externo, oferecendo características como flexibilidade e interoperabilidade aos sistemas integrados. O ROS2 implementa um protocolo de comunicação, de nome DDS [49], que, para além de garantir serviços de comunicação, implementa a especificação DDS-Security, que oferece diferentes métodos de adoção de segurança, através de uma metodologia de plugins. Através do uso desta especificação, juntamente com o uso do toolset SROS2, é possível configurar o ROS2 de forma a proporcionar um ambiente seguro às aplicações integradas. O presente trabalho foca-se no estudo e deteção de problemas de segurança em topologias ROS2, através da verificação formal de propriedades de segurança. No entanto, a segurança é um assunto extenso, pelo que o foco de interesse nesta tese é numa propriedade particular de segurança para mostrar a viabilidade da presente técnica, de nome OD. Esta dissertação introduz a uma ferramenta de verificação de nome svROS, que contempla múltiplas funcionalidades para suportar este tipo de análise usando Alloy [32], uma linguagem de especificação formal e respectiva ferramenta de análise., This work is financed by National Funds through the Portuguese funding agency, FCT - Fundação para a Ciência e a Tecnologia, within project LA/P/0063/2020.

The Tokeneer project was an initiative set forth by the National Security Agency (NSA, USA) to be used as a demonstration that developing highly secure systems can be made by applying rigorous methods in a cost-effective manner. Altran UK was selected by NSA to carry out the development of the Tokeneer ID Station. The company wrote a Z specification later implemented in the SPARK Ada programming language, which was verified using the SPARK Examiner toolset. In this paper, we show that the Z specification can be readily and naturally encoded in the $$\{log\}$$ set constraint language, thereby generating a functional prototype. Furthermore, we show that $$\{log\}$$ ’s automated proving capabilities can discharge all the proof obligations concerning state invariants as well as important security properties. As a consequence, the prototype can be regarded as correct with respect to the verified properties. This provides empirical evidence that Z users can use $$\{log\}$$ to generate correct prototypes from their Z specifications. In turn, these prototypes enable or simplify some verification activities discussed in the paper.

Blockchain technology has been known as a cryptocurrency platform since the emergence of its first and largest application, bitcoin. Blockchain contributes to the process of changing low-trust centralized transaction ledger held by a single third party, to high-trust decentralized form held by different verifying nodes. Due to its decentralized nature and security robustness, blockchain has big potentials to be applied in various fields beyond cryptocurrency. This paper aims to provide readers a more complete literature review of blockchain, compared with existing works. We introduce and explain various security properties of blockchain, provide a taxonomy of blockchain-based applications, and discuss challenges of blockchain in terms of security and performance. Furthermore, some research directions are given in the last section of the paper.

Trusted Execution Environments ('TEEs') or 'secure enclaves' aim at enabling more secure computation and data management. There is much enthusiasm for this technology, not least as we see increasing legal and regulatory attention on issues of security, privacy, and data management and use. With cloud providing the infrastructure for underpinning applications, data processing and analytics/ML, access to enclaves and enclave-backed technologies are increasingly being offered by service (cloud) providers - with the technology described as enabling confidential computing . This paper provides a high-level overview of the common security properties provided by enclaves, and considers how such technology, in being offered by cloud providers, relates to organizational legal and regulatory concerns. Focusing on data protection regulations, we explore the aspects of TEEs that might assist compliance, and who stands to benefit from the deployment of such technology in a service provision context.

The paper is devoted to the actual problem of ensuring privacy during performing transactions in distributed ledgers. We discuss various aspects of transaction privacy, as well as the specifics of setting the problem for distributed ledgers with two main models for representing participants' balances: the UTXO-model and the account model. Based on these results, we outline definitions and consider security properties of the main cryptographic primitives used for preserving the privacy of transactions: mixers, ring signatures, homomorphic encryption, and zero-knowledge proofs. We analyze well-known solutions for distributed ledgers based on the UTXO-model, such as Zcash, Monero, Zcoin, Dash, CoinShuffle, Verge, Grin, and others, as well as for systems based on the account model: DSC, Zether, Zeth, BlockMaze. Based on the comparison of advantages, disadvantages, and limitations for existing solutions, conclusions are drawn about the future development of distributed ledgers that ensure the privacy of transactions, and new research tasks are outlined.

Almost 50 years ago, D. E. Bell and L. LaPadula published the first formal model of a secure system, known today as the Bell–LaPadula (BLP) model. BLP is described as a state machine by means of first-order logic and set theory. The authors also formalize two state invariants known as security condition and *-property. Bell and LaPadula prove that all the state transitions preserve these invariants. In this paper we present a fully automated proof of the security condition and the *-property for all the model operations. The model and the proofs are coded in the $$\{log\}$$ tool. As far as we know this is the first time such proofs are automated. Besides, we show that the $$\{log\}$$ model is also an executable prototype. Therefore we are providing an automatically verified executable prototype of BLP.

To assess the quality and security of cryptographic protocols, we use various formal verification tools, such as Scyther tool, Avispa, ProVerif. these formal verifiers can check the protocol for vulnerability to attacks on secrecy and authentication, as these are the most prevalent attacks on protocols. However, this is not enough to fully analyze the security of the protocol. In this article, we will use linear temporal logic (LTL) model checking with SPIN. This tool, unlike the formal verifiers listed above, is not designed for a specific application in the context of cryptographic protocols; however, it has a very wide range of possibilities. In particular, for each security property, it is possible to describe the behavior of an attacker and test for the stability of the protocol model to its various attacks. The purpose of this work is to describe the developed methodology for verifying the security of authentication properties using the SPIN verifier.

The service of authentication constitutes the spine of all security properties. It is the phase where entities prove their identities to each other and generally establish and derive cryptographic keys to provide confidentiality, data integrity, non-repudiation, and availability. Due to the heterogeneity and the particular security requirements of IoT (Internet of Things), developing secure, low-cost, and lightweight authentication protocols has become a serious challenge. This has excited the research community to design and develop new authentication protocols that meet IoT requirements. An interesting hardware technology, called PUFs (Physical Unclonable Functions), has been the subject of many subsequent publications on lightweight, low-cost, and secure-by-design authentication protocols. This has turned our attention to investigate the most recent PUF-based authentication protocols for IoT. In this paper, we review the security of these protocols. We first provide the necessary background on PUFs, their types, and related attacks. Also, we discuss how PUFs are used for authentication. Then, we analyze the security of PUF-based authentication protocols to identify and report common security issues and design flaws, as well as to provide recommendations for future authentication protocol designers.

This paper systematizes knowledge about secure software supply chain patterns. It identifies four stages of a software supply chain attack and proposes three security properties crucial for a secured supply chain: transparency, validity, and separation. The paper describes current security approaches and maps them to the proposed security properties, including research ideas and case studies of supply chains in practice. It discusses the strengths and weaknesses of current approaches relative to known attacks and details the various security frameworks put out to ensure the security of the software supply chain. Finally, the paper highlights potential gaps in actor and operation-centered supply chain security techniques.

International audience; Systems engineering, or engineering in general, has long been relying on document-centric approaches. Switching to model-based systems engineering, or MBSE for short, has extensively been discussed over the past three decades. Since about two decades, MBSE has been commonly associated with the modeling language SysML (Systems Modeling Language), which offers a standardized notation, not a methodology of using it. SysML needs therefore to be associated with a methodology supported by tools. In this paper, a methodology supported by the free and open-source software TTool is associated with SysML. This paper focuses discussion on methodological issues, leading the authors to share their experience in real-time systems modeling. Modeling with SysML is more than just drawing the different diagrams. Associated tools offer possibilities to analyze SysML models for specific properties. In this paper, verification addresses both safety and security properties. The TTool model checker inputs the SysML model enriched with safety properties to be verified and outputs an yes/no answer for each property. Security verification checks SysML models against confidentiality, integrity, and authenticity properties. As an illustration of the proposed approach, an aircraft cockpit door control system is modeled in SysML and verified against safety and security properties.

A leader election or consensus protocol for distributed systems is the process of selecting a leader among a group of entities to handle the decision around what information should be added to the ledger. With the advent of blockchain, several consensus protocols have been proposed to overcome the issues of the Bitcoin Proof-of-Work consensus protocol such as intensive power consumption and selfish strategies. In this paper, we propose a new leader election protocol that relies on external random number generator (RNG) services named Leader Election Protocol based on Trusted RNG Service Providers (LEP-TSP). External RNG services enable to reduce computation cost to elect a leader and strengthen the fairness requirement of uniform probability of being leader. First, we present a formal model of LEP-TSP based on the model proposed by Boneh et al. on the Single secret leader election. Then, we provide a construction of LEP-TSP and show that it achieves required security properties while more than 2/3 of participants are honest.

A security metric evaluates the security performance, goals, and objectives of software and provides information that helps in the assessment of software security. With the advancement in technology, software is faced with lots of threats and risks to customers’ data and privacy. Most of these threats are a result of security being considered as a feature of software and not taking it into account during the development of the software. Security metrics obtained during the development process go a long way to improve the core security properties of software, that is: confidentiality, integrity, and availability. Thus, it is of obvious importance to consider security across the software development lifecycle, hence, the use of software security metrics. This paper reviews the various security metrics that are meditated in the copious phases during the progression of the lifecycle with the aim of providing practitioners, managers, and researchers the substantial knowledge for further security assessment.

Security Assurance Cases (SAC) are a form of structured argumentation used to reason about the security properties of a system. After the successful adoption of assurance cases for safety, SAC are getting significant traction in recent years, especially in safety-critical industries (e.g., automotive), where there is an increasing pressure to be compliant with several security standards and regulations. Accordingly, research in the field of SAC has flourished in the past decade, with different approaches being investigated. In an effort to systematize this active field of research, we conducted a systematic literature review (SLR) of the existing academic studies on SAC. Our review resulted in an in-depth analysis and comparison of 51 papers. Our results indicate that, while there are numerous papers discussing the importance of SAC and their usage scenarios, the literature is still immature with respect to concrete support for practitioners on how to build and maintain a SAC. More importantly, even though some methodologies are available, their validation and tool support is still lacking.

The Algorand consensus protocol, introduced by Chen and Micali in 2016, uses a pure proof-of-stake protocol based on Byzantine agreement rather than the well-known Bitcoin proof-of-work. In this paper, we analyze specific security properties of Algorand related to "unpredictability". The unpredictability property has been initially defined by Boneh et al. in the context of single secret leader election. We show that Algorand satisfies the original unpredictability property. Then, we extend the unpredictability property to a more generic property referred to as "t-forward unpredictability" and show that for a particular setting of Algorand, the t-forward unpredictability property is not satisfied. Specifically, we provide a strategy enabling to predict the future leaders.

Modern digital signature schemes can provide more guarantees than the standard notion of (strong) unforgeability, such as offering security even in the presence of maliciously generated keys, or requiring to know a message to produce a signature for it. The use of signature schemes that lack these properties has previously enabled attacks on real-world protocols. In this work we revisit several of these notions beyond unforgeability, establish relations among them, provide the first formal definition of non re-signability, and a transformation that can provide these properties for a given signature scheme in a provable and efficient way.Our results are not only relevant for established schemes: for example, the ongoing NIST PQC competition towards standardizing post-quantum signature schemes has six finalists in its third round. We perform an in-depth analysis of the candidates with respect to their security properties beyond unforgeability. We show that many of them do not yet offer these stronger guarantees, which implies that the security guarantees of these post-quantum schemes are not strictly stronger than, but instead incomparable to, classical signature schemes. We show how applying our transformation would efficiently solve this, paving the way for the standardized schemes to provide these additional guarantees and thereby making them harder to misuse.

All-or-nothing transforms have been defined as bijective mappings on all s-tuples over a specified finite alphabet. These mappings are required to satisfy certain "perfect security" conditions specified using entropies of the probability distribution defined on the input s-tuples. Alternatively, purely combinatorial definitions of AONTs have been given, which involve certain kinds of "unbiased arrays". However, the combinatorial definition makes no reference to probability definitions. In this paper, we examine the security provided by AONTs that satisfy the combinatorial definition. The security of the AONT can depend on the underlying probability distribution of the s-tuples. We show that perfect security is obtained from an AONT if and only if the input s-tuples are equiprobable. However, in the case where the input s-tuples are not equiprobable, we still achieve a weaker security guarantee. We also consider the use of randomized AONTs to provide perfect security for a smaller number of inputs, even when those inputs are not equiprobable.

Internet of Things (IoT) devices rely upon remote firmware updates to fix bugs, update embedded algorithms, and make security enhancements. Remote firmware updates are a significant burden to wireless IoT devices that operate using low-power wide-area network (LPWAN) technologies due to slow data rates. One LPWAN technology, Long Range (LoRa), has the ability to increase the data rate at the expense of range and noise immunity. The optimization of communications for maximum speed is known as adaptive data rate (ADR) techniques, which can be applied to accelerate the firmware update process for any LoRa-enabled IoT device. In this paper, we investigate ADR techniques in an application that provides remote monitoring of cattle using small, battery-powered devices that transmit data on cattle location and health using LoRa. In addition to issues related to firmware update speed, there are significant concerns regarding reliability and security when updating firmware on mobile, energy-constrained devices. A malicious actor could attempt to steal the firmware to gain access to embedded algorithms or enable faulty behavior by injecting their own code into the device. A firmware update could be subverted due to cattle moving out of the LPWAN range or the device battery not being sufficiently charged to complete the update process. To address these concerns, we propose a secure and reliable firmware update process using ADR techniques that is applicable to any mobile or energy-constrained LoRa device. The proposed system is simulated and then implemented to evaluate its performance and security properties.

We present Pay To Transport (P2T), a protocol that lets customers buy an item remotely in an atomic, privacy preserving and trustless manner. P2T needs only basic features of a blockchain scripting language and does not need any tracking systems, arbitrator or deposit to preserve its security properties. For this reason the protocol can be implemented on any permissionless blockchain, regardless of its scripting language, without additional trust. Merchants’ and transporters’ addresses are public, but in P2T the parties never pay those addresses directly. Therefore P2T maintains the privacy of customers, merchant and transporters.

An evaluation of safety and security properties performed by an independent organisation can be an important step towards establishing trust in Automated Driving Systems (ADS), bridging the gap between the marketing portrayal and the actual performance of such systems in real operating conditions. However, due to the complexity of an ADS’s behaviour and dangers involved in performing real environment security attacks, we believe assessments that can be performed with a combination of simulation and validation at test facilities is the way forward.In this paper, we outline an approach to derive test suites applicable to generic ADS feature classes, where classes would have similar capabilities and comparable assessment results. The goal is to support black box testing of such feature classes as part of an independent evaluation. By the means of co-simulation of post-attack behaviour and critical scenarios, we derive a representative set of physical certification tests, to gain an understanding of the interplay between safety and security. During the initial tests an ADS is subjected to various attacks and its reactions recorded. These reactions such as reduced functionality, fall back etc., together with relevant scenarios for the class is further analysed to check for safety implications. HEADSTART

A primary concern in the design and development of a RESTful Application Programming Interfaces (APIs) is API security. A RESTful API provides data over the network using HTTP and must not violate any of its security properties. When APIs are designed, the functional and security properties are inextricably linked thus security requirements of an API cannot be treated as afterthoughts. We therefore propose an approach to specifying and verifying APIs functional and security requirements with the practical formal method SOFL (Structured-Object-oriented Formal Language). We convert an API specification written in an API description language into SOFL while expressing security requirements as constraints on the APIs functional requirements and dataflow between the API’s trust boundaries. The verification of the specifications can be carried out using specification-based conformance testing. We apply this approach to a model of an online banking API as a case study using Django REST Framework and analyze its results.

In the previous chapters we studied constructions of hash functions in the unkeyed (resp. publicly keyed) setting for security properties such as collision resistance or second-preimage resistance.

The IETF is standardizing an authenticated key establishment (AKE) protocol named EDHOC for constrained IoT devices. In contrast to more powerful devices like web cameras and cars, which receive a lot of media attention, such devices operate under severe energy consumption and message size restrictions. EDHOC was first formally analyzed in 2018 by Bruni et al. Since then, the protocol has been significantly extended and now has three new key establishment methods. In this paper, we formally analyze all methods of EDHOC in a symbolic Dolev-Yao model, using the Tamarin verification tool. We show that the different methods provide sensible, but also rather heterogeneous security properties, and discuss various consequences of this. Our work has also led to improvements in the design and the specification of EDHOC.

Decentralized finance (DeFi) has become one of the most successful applications of blockchain and smart contracts. The DeFi ecosystem enables a wide range of crypto-financial activities, while the underlying smart contracts often contain bugs, with many vulnerabilities arising from the unforeseen consequences of composing DeFi protocols together. In this paper, we propose a formal process-algebraic technique that models DeFi protocols in a compositional manner to allow for efficient property verification. We also conduct a case study to demonstrate the proposed approach in analyzing the composition of two interacting DeFi protocols, namely, Curve and Compound. Finally, we discuss how the proposed modeling and verification approach can be used to analyze financial and security properties of interest.

This paper presents the experience of verifying server implementations of the TLS cryptographic protocol version 1.3. TLS is a widely used cryptographic protocol designed to create secure data transmission channels and provides the necessary functionality for this: confidentiality of the transmitted data, data integrity, and authentication of the parties. The new version 1.3 of the TLS protocol was introduced in August 2018 and has a number of significant differences compared to the previous version 1.2. A number of TLS developers have already included support for the latest version in their implementations. These circumstances make it relevant to do research in the field of verification and security of the new TLS protocol implementations. We used a new test suite for verifying implementations of the TLS 1.3 for compliance with Internet specifications, developed on the basis of the RFC8446, using UniTESK technology and mutation testing methods. The current work is part of the TLS 1.3 protocol verification project and covers some of the additional functionality and optional protocol extensions. To test implementations for compliance with formal specifications, UniTESK technology is used, which provides testing automation tools based on the use of finite state machines. The states of the system under test define the states of the state machine, and the test effects are the transitions of this machine. When performing a transition, the specified impact is passed to the implementation under test, after which the implementation's reactions are recorded and a verdict is automatically made on the compliance of the observed behavior with the specification. Mutational testing methods are used to detect non-standard behavior of the system under test by transmitting incorrect data. Some changes are made to the protocol exchange flow created in accordance with the specification: either the values of the message fields formed on the basis of the developed protocol model are changed, or the order of messages in the exchange flow is changed. The protocol model allows one to make changes to the data flow at any stage of the network exchange, which allows the test scenario to pass through all the significant states of the protocol and in each such state to test the implementation in accordance with the specified program. So far, several implementations have been found to deviate from the specification. The presented approach has proven effective in several of our projects when testing network protocols, providing detection of various deviations from the specification and other errors.

Arpanet, Internet, Internet of Services, Internet of Things, Internet of Skills. What next? We conjecture that in a few years from now, we will have the Internet of Neurons, in which humans will be able to connect bi-directionally to the net using only their brain. The Internet of Neurons will provide new, tremendous opportunities thanks to constant access to unlimited information, but it will also bring along enormous challenges, especially concerning security, privacy and trust. In this paper we discuss the main technological (and neurological) breakthroughs required to enable the Internet of Neurons, the new opportunities it provides and the security challenges it raises. We also elaborate on the novel system models, threat models and security properties that are required to reason about privacy, security and trust in the Internet of Neurons.

Blockchain technology has come a long way since its inception in the form of Bitcoin in 2009. With a growing interest from industry and academia came an influx of new application areas and domains that make use of this technology on a daily basis. This technology, while having unique security properties, also presented new security challenges and previously unexplored attack vectors that became the target of malicious actors in the domain.

We describe how a probabilistic Hoare logic with localities can be used for reasoning about security. As a proof-of-concept, we analyze Vernam and El-Gamal cryptosystems, prove the security properties that they do satisfy, and disprove those that they do not. We also consider a version of the Muddy Children puzzle, where children’s trust and noise are taken into account.

Our society has become more dependent on software-intensive systems, such as Information and Communication Technologies (ICTs) systems, to perform their daily tasks (sometimes critical). However, in most cases, organizations and particularly small ones place limited value on information and its security. In the same time, achieving security in such systems is a difficult task because of the increasing complexity and connectivity in ICT development. In addition, security has impacts on many attributes such as openness, safety and usability. Thus, security becomes a very important aspect that should be considered in early phases of development. In this work, we propose an approach in order to secure ICT software architectures during their development by considering two visions to formulate security statements using the negative view, as the study of threats (e.g., usurpation) and positive view as the study of the security objectives (e.g., confidentiality). The contributions of this work are threefold: (1) an integrated design framework for the specification and analysis of reusable (formal) model libraries for secure software architectures; (2) a novel model-based methodology for developing secure software architecture by reuse; and (3) a set of supporting tools. The approach associates Model-Driven Engineering (MDE) and formal techniques to design a set of modeling languages for specifying and analyzing architecture and property models which allows reuse of capitalized security-related know-how. The results are provided as two complementary artifacts: (a) a process of development of reusable formal model libraries for the specification and verification of security threats and objectives by a security expert; and (b) a process of secure architectural design and analysis by an architect reusing the libraries specified in the process (a). Process (a) includes the following activities: (1) the formal specification of the security threats and objectives as the properties of a model using technology-independent specification language; (2) the interpretation of the resulted model libraries in a tooled formal language; and (3) the definition of security policies as abstract security countermeasures to ensure security properties. Process (b) includes the following activities: (1) security analysis of a concrete architecture model to verify the security requirements and identify security issues reusing the property models; [...], Notre société est devenue plus dépendante des systèmes logiciels complexes, tels que les systèmes de technologies de l'information et de la communication (TIC), pour effectuer des tâches quotidiennes (parfois critiques). Cependant, dans la plupart des cas, les organisations et particulièrement les plus petites placent une valeur limitée sur les données et leur sécurité. Dans le même temps, la sécurité de ces systèmes est une tâche difficile en raison de la complexité et connectivité croissante dans le développement des TIC. De plus, la sécurité a une incidence sur de nombreux attributs tels que la transparence, la sureté et l'utilisabilité. Ainsi, la sécurité devient un aspect très important qui devrait être pris en compte dans les premières phases du cycle de développement. Dans ce travail, nous proposons une approche afin de sécuriser les architectures logicielles des TIC pendant leur développement en considérant la vision positive, qui se manifeste par l'étude des objectifs de sécurité (ex., confidentialité), et la vision négative, qui se manifeste par l'étude des menaces (ex., usurpation). Les contributions de ce travail sont triples : (1) un framework de conception intégré pour la spécification et l'analyse de bibliothèques de modèles (formels) réutilisables pour les architectures logicielles sécurisées ; (2) une nouvelle méthodologie basée sur les modèles pour développer une architecture logicielle sécurisée par réutilisation ; et (3) une suite d'outils support. L'approche associe l'ingénierie dirigée par les modèles (IDM) et les techniques formelles pour concevoir un ensemble de langages de modélisation afin de spécifier et analyser des modèles d'architecture et de propriétés permettant la réutilisation et ainsi capitaliser un savoir-faire en matière de sécurité. Les résultats sont fournis sous forme de deux artéfacts complémentaires : (a) un processus de développement de bibliothèques de modèles réutilisables pour la spécification et la vérification d'objectifs et de menaces de sécurité par un expert en sécurité ; et (b) un processus de conception d'architecture sécurisé par un architecte s'appuyant sur les bibliothèques spécifiées dans le processus (a). Le processus (a) comprend les activités suivantes : (1) la spécification formelle d'objectifs et de menaces de sécurité comme propriétés d'un modèle en utilisant un langage de spécification indépendant technologiquement ; (2) l'interprétation des bibliothèques de modèles résultants dans un langage formel outillé ; et (3) la définition de politiques de sécurité en tant que solutions abstraites de sécurité pour assurer les propriétés de sécurité. Le processus (b) comprend les activités suivantes : (1) l'analyse d'un modèle d'architecture concret afin de vérifier les exigences et d'identifier les problèmes de sécurité en réutilisant les modèles de propriétés[...]