Difference between revisions of "IoTSec:T2.3"
From its-wiki.no
Josef.Noll (Talk | contribs) (Created page with "{{Task |Title=Formal technologies for semantic provability |Page Title=T2.3 Semantic Provability |Workpackage=IoTSec:WP2 |Lead partner=Ifi |Partner=UNIK, Ifi, |Objective=This...") |
|||
(11 intermediate revisions by 2 users not shown) | |||
Line 4: | Line 4: | ||
|Workpackage=IoTSec:WP2 | |Workpackage=IoTSec:WP2 | ||
|Lead partner=Ifi | |Lead partner=Ifi | ||
− | |Partner=UNIK, | + | |Partner=UNIK, NR |
|Objective=This task will establish formal technologies for semantic provability | |Objective=This task will establish formal technologies for semantic provability | ||
}} | }} | ||
+ | |||
+ | = Detailed objectives = | ||
+ | The main objective is to give guarantees for relevant security properties. | ||
+ | By utilizing automatic decision algorithms from logic and formal methods | ||
+ | we will build tool support for automated proofs. | ||
+ | This will increase the robustness of the smart grid system. | ||
+ | This includes: | ||
+ | * formulating dependability and security requirements | ||
+ | * usage of suitable metrics of system quality and behaviour | ||
+ | * investigation of static and dynamic techniques. | ||
+ | The work on security metrics and security properties will involve our partner | ||
+ | prof. Issa Traore, University of Victoria, Canada. | ||
+ | |||
+ | = Detailed work = | ||
+ | Initial work consists of | ||
+ | investigation of | ||
+ | the integration of the semantic model and provability mechanisms. | ||
+ | The next phase of the work is | ||
+ | development of automated tools, | ||
+ | while ensuring their usability in smart grid systems. This includes: | ||
+ | * investigation of permitted and malicious actions | ||
+ | * techniques for ensuring robustness and security properties | ||
+ | * investigation of time-related and probabilistic methods. | ||
+ | |||
+ | = Expected results = | ||
+ | This task has the following expected results: | ||
+ | * [[has result::a minimum of 3 papers, including one journal paper (M12-36)]] | ||
+ | * [[has result::a non-trivial case study (M12)]] | ||
+ | * [[has result::a tool for semantic provability (M48)]] | ||
+ | |||
+ | <!-- = earlier input = | ||
+ | = Contributions = | ||
+ | Olaf: I may contribute to the last part, focusing on automated deductive reasoning, and follow the other two points - ''leadership?'' | ||
+ | |||
+ | ....and ensure that decisions made are not violating certain poperties. | ||
+ | |||
+ | Undecided: How much is static and how much is dynamic (at run-time)? | ||
+ | |||
+ | Josef: Reasoning over models | ||
+ | |||
+ | --> | ||
+ | |||
+ | == References == | ||
+ | <references> |
Latest revision as of 14:53, 27 August 2015
Security in IoT for Smart Grids | |||||||
---|---|---|---|---|---|---|---|
|
![]() |
T2.3 Semantic Provability
Task Title | Formal technologies for semantic provability |
---|---|
WP | IoTSec:WP2 |
Lead partner | Ifi |
Leader | |
Contributors | UNIK, NR |
edit this task |
Objective
This task will establish formal technologies for semantic provability
Category:Task |
Deliverables in T2.3 Semantic Provability
Title | Due month | Lead partner | Editor | Dissemination level | |
---|---|---|---|---|---|
D2.3.1 | Semantic Provability Framework (draft) | M24 | Ifi | Olaf Owe | Public |
D2.3.2 | Semantic Provability Framework (final) | M36 | Ifi | Olaf Owe | Public |
D2.3.3 | Semantic Provability applied to Smart Grids | M48 | Ifi | Olaf Owe | Public |
Detailed objectives
The main objective is to give guarantees for relevant security properties. By utilizing automatic decision algorithms from logic and formal methods we will build tool support for automated proofs. This will increase the robustness of the smart grid system. This includes:
- formulating dependability and security requirements
- usage of suitable metrics of system quality and behaviour
- investigation of static and dynamic techniques.
The work on security metrics and security properties will involve our partner prof. Issa Traore, University of Victoria, Canada.
Detailed work
Initial work consists of investigation of the integration of the semantic model and provability mechanisms. The next phase of the work is development of automated tools, while ensuring their usability in smart grid systems. This includes:
- investigation of permitted and malicious actions
- techniques for ensuring robustness and security properties
- investigation of time-related and probabilistic methods.
Expected results
This task has the following expected results:
- a minimum of 3 papers, including one journal paper (M12-36)
- a non-trivial case study (M12)
- a tool for semantic provability (M48)
References