Security property modeling
| Autor: | Hiba Hnaini, Joël Champeau, Luka Le Roux, Ciprian Teodorov |
|---|---|
| Přispěvatelé: | Equipe Processes for Safe and Secure Software and Systems (Lab-STICC_P4S), Laboratoire des sciences et techniques de l'information, de la communication et de la connaissance (Lab-STICC), École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-École Nationale d'Ingénieurs de Brest (ENIB)-Université de Bretagne Sud (UBS)-Université de Brest (UBO)-École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne)-Institut Mines-Télécom [Paris] (IMT)-Centre National de la Recherche Scientifique (CNRS)-Université Bretagne Loire (UBL)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT), École Nationale Supérieure de Techniques Avancées Bretagne (ENSTA Bretagne) |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: | |
| Zdroj: | 7th International Conference on Information Systems Security and Privacy, ICISSP 2021 7th International Conference on Information Systems Security and Privacy, ICISSP 2021, Feb 2021, Vienne-Virtual Online, Austria. pp.694-701, ⟨10.5220/0010388206940701⟩ ICISSP |
| Popis: | International audience; With the increasing number of cyber-attacks on cyber-physical systems, many security precautions and solutions have been suggested. However, most of these solutions aim to prevent the access of an adversary to the system. Though, with the increasing number of elements used in a system, and thus vulnerabilities, it is essential to study the risks introduced to the system to make the system itself efficient enough to react to the attacks once an attacker has obtained access. Analyzing and discovering the risks is the first step to making the system more resilient. This paper proposes a methodology that combines the qualitative risk analysis with formal methods (model checking) to identify the risks that were not recognized during testing or functional modeling phases. To examine this methodology, a car reservation system is modeled with an attacker, and then its security properties are verified using UPPAAL model checking tool. As a result, some risks were identified and tested for the possibility of them occurring and their effects on the system. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|