liu.seSearch for publications in DiVA
Change search
Link to record
Permanent link

Direct link
BETA
Nadjm-Tehrani, SiminORCID iD iconorcid.org/0000-0002-1485-0802
Alternative names
Publications (10 of 126) Show all publications
Törnblom, J. & Nadjm-Tehrani, S. (2020). Formal Verification of Input-Output Mappings of Tree Ensembles. Science of Computer Programming, 194
Open this publication in new window or tab >>Formal Verification of Input-Output Mappings of Tree Ensembles
2020 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 194Article in journal (Refereed) Published
Abstract [en]

Recent advances in machine learning and artificial intelligence are now beingconsidered in safety-critical autonomous systems where software defects maycause severe harm to humans and the environment. Design organizations in thesedomains are currently unable to provide convincing arguments that their systemsare safe to operate when machine learning algorithms are used to implement theirsoftware.

In this paper, we present an efficient method to extract equivalence classes from decision trees and tree ensembles, and to formally verify that their input-output mappings comply with requirements. The idea is that, given that safety requirements can be traced to desirable properties on system input-output patterns, we can use positive verification outcomes in safety arguments.

This paper presents the implementation of the method in the tool VoTE (Verifier of Tree Ensembles), and evaluates its scalability on two case studies presented in current literature. We demonstrate that our method is practical for tree ensembles trained on low-dimensional data with up to 25 decision trees and tree depths of up to 20.Our work also studies the limitations of the method with high-dimensionaldata and preliminarily investigates the trade-off between large number of trees and time taken for verification.

Keywords
Formal verification, Decision tree, Tree ensemble, Random forest, Gradient boosting machine
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-164563 (URN)10.1016/j.scico.2020.102450 (DOI)
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2020-03-24 Created: 2020-03-24 Last updated: 2020-03-31
Da Fontoura, A. A., Nascimento, F. M., Nadjm-Tehrani, S. & De Freitas, E. P. (2020). Timing Assurance of Avionic Reconfiguration Schemes using Formal Analysis. IEEE Transactions on Aerospace and Electronic Systems, 56(1), 95-106
Open this publication in new window or tab >>Timing Assurance of Avionic Reconfiguration Schemes using Formal Analysis
2020 (English)In: IEEE Transactions on Aerospace and Electronic Systems, ISSN 0018-9251, E-ISSN 1557-9603, IEEE Transactions on Aerospace and Electronic Systems, E-ISSN 1557-9603, Vol. 56, no 1, p. 95-106Article in journal (Refereed) Published
Abstract [en]

Reconfigurable avionics systems can tolerate faults by moving functionalities from failed components to another available system component. This paper proposes a distributed reconfigurable architecture for application migration from failed modules to working ones. The feasible system reconfiguration states are determined off-line to provide the expected configuration in foreseen situations. Model Checking is used to determine feasible configurations evaluating specific temporal properties. A case study is used to show the application of the presented approach as a proof of concept

Place, publisher, year, edition, pages
IEEE, 2020
Keywords
Reconfiguration, Avionic Systems, Distributed RealTime Embedded Systems, Schedulability Analysis, Model Check-ing
National Category
Embedded Systems
Identifiers
urn:nbn:se:liu:diva-161755 (URN)10.1109/TAES.2019.2915406 (DOI)000515747100008 ()
Note

Funding agencies: Swedish Governmental Agency for Innovation SystemsVinnova [NFFP7-04890]; Brazilian National Council for Scientific and Technological Development (CNN)

Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2020-03-19Bibliographically approved
Periera, D. P., Hirata, C. & Nadjm-Tehrani, S. (2019). A STAMP-based ontology approach to support Safety and Security. Journal of Information Security and Applications, 47, 302-319
Open this publication in new window or tab >>A STAMP-based ontology approach to support Safety and Security
2019 (English)In: Journal of Information Security and Applications, ISSN 2214-2134, E-ISSN 2214-2126, Journal of Information Security and Applications Analyses, Vol. 47, p. 302-319Article in journal (Refereed) Published
Abstract [en]

Considerations of safety and security in the early stage of system life cycle are essential to collect and prioritize operation needs, determine feasibility of the desired system, and identify technology gaps. Experts from many disciplines are needed to perform the safety and security analyses, ensuring that a system has the necessary attributes. Safety assessment is usually conducted in the concept stage. On the order hand, security assessment is performed in design stage usually when an initial architecture along with the logical and physical components are defined. Systems-Theoretic Process Analysis (STPA) is a new hazard analysis technique based on systems thinking and is built on top of a new causality model of accident, which stands for Systems-Theoretic Accident Model and Processes (STAMP), grounded in systems theory. STPA for Security (STPA-Sec) is an extension of STPA that proposes to include security concerns into the analysis. STPA-Sec helps identifying some hazardous control actions, causal scenarios, and casual factors; however, no emphasis is placed on security threat scenarios. In this paper we propose an ontology-based technique that extends STPA-Sec to improve identification of causal scenarios and associated casual factors, specifically those related to security. We propose an approach that assists safety and security experts conducting safety and security analyses using STPA-Sec with a supporting ontology. First, we present an ontology representing the safety and security knowledge through STPA-Sec process, and provide a tool that implements the proposed ontology. We then propose a process to capture safety and security knowledge into the proposed ontology to identify causal scenarios. We perform a preliminary evaluation of the ontology and the process using an aeronautic case study. The results show that the ontology-based approach helps systems engineers to identify more security scenarios compared to the case where they use only STPA-Sec. Furthermore, some hazardous control actions are not addressed if the systems engineer uses the basic STPA-Sec.

Place, publisher, year, edition, pages
Elsevier, 2019
National Category
Computer Systems
Identifiers
urn:nbn:se:liu:diva-161754 (URN)10.1016/j.jisa.2019.05.014 (DOI)000480387600032 ()2-s2.0-85066634864 (Scopus ID)
Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2019-11-14Bibliographically approved
Törnblom, J. & Nadjm-Tehrani, S. (2019). An Abstraction-Refinement Approach to Formal Verification of Tree Ensembles. In: Computer Safety, Reliability, and Security: SAFECOMP 2019 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Turku, Finland, September 10, 2019, Proceedings. Paper presented at ​Second International Workshop on Artificial Intelligence Safety Engineering (pp. 301-313). Springer
Open this publication in new window or tab >>An Abstraction-Refinement Approach to Formal Verification of Tree Ensembles
2019 (English)In: Computer Safety, Reliability, and Security: SAFECOMP 2019 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Turku, Finland, September 10, 2019, Proceedings, Springer, 2019, p. 301-313Conference paper, Published paper (Refereed)
Abstract [en]

Recent advances in machine learning are now being considered for integration in safety-critical systems such as vehicles, medical equipment and critical infrastructure. However, organizations in these domains are currently unable to provide convincing arguments that systems integrating machine learning technologies are safe to operate in their intended environments.

In this paper, we present a formal verification method for tree ensembles that leverage an abstraction-refinement approach to counteract combinatorial explosion. We implemented the method as an extension to a tool named VoTE, and demonstrate its applicability by verifying the robustness against perturbations in random forests and gradient boosting machines in two case studies. Our abstraction-refinement based extension to VoTE improves the performance by several orders of magnitude, scaling to tree ensembles with up to 50 trees with depth 10, trained on high-dimensional data.

Place, publisher, year, edition, pages
Springer, 2019
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11699
Keywords
Formal verification, Decision trees, Tree ensembles
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-160869 (URN)10.1007/978-3-030-26250-1_24 (DOI)978-3-030-26249-5 (ISBN)
Conference
​Second International Workshop on Artificial Intelligence Safety Engineering
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2019-10-11 Created: 2019-10-11 Last updated: 2019-11-14
Hirata, C. & Nadjm-Tehrani, S. (2019). Combining GSN and STPA for Safety Arguments. In: Proceedings of the 7th International workshop on Assurance Cases for Software-intensive Systems (ASSURE), held in conjunction with SAFECOMP: . Paper presented at SAFECOMP 2019 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Turku, Finland, September 10, 2019. Springer
Open this publication in new window or tab >>Combining GSN and STPA for Safety Arguments
2019 (English)In: Proceedings of the 7th International workshop on Assurance Cases for Software-intensive Systems (ASSURE), held in conjunction with SAFECOMP, Springer, 2019Conference paper, Published paper (Refereed)
Abstract [en]

Dependability case, assurance case, or safety case is employed to explain why all critical hazards have been eliminated or adequately mitigated in mission-critical and safety-critical systems. Goal Structuring Notation (GSN) is the most employed graphical notation for documenting dependability cases. System Theoretic Process Analysis (STPA) is a technique, based on System Theoretic Accidents Model and Process (STAMP), to identify hazardous control actions, scenarios, and causal factors. STPA is considered a rather complex technique, but there is a growing interest in using STPA in certifications of safety-critical systems development. We investigate how STAMP and STPA can be related to use of assurance cases. This is done in a generic way by representing the STPA steps as part of the evidence and claim documentations within GSN.

Place, publisher, year, edition, pages
Springer, 2019
Keywords
Safety assurance, GSN, Assurance case, STAMP, STPA
National Category
Other Engineering and Technologies not elsewhere specified
Identifiers
urn:nbn:se:liu:diva-161758 (URN)10.1007/978-3-030-26250-1_1 (DOI)2-s2.0-85072885947 (Scopus ID)
Conference
SAFECOMP 2019 Workshops, ASSURE, DECSoS, SASSUR, STRIVE, and WAISE, Turku, Finland, September 10, 2019
Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2019-11-18Bibliographically approved
Törnblom, J. & Nadjm-Tehrani, S. (2019). Formal Verification of Random Forests in Safety-Critical Applications. In: Formal Techniques for Safety-Critical Systems: . Paper presented at Sixth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2018), Gold Coast, Australia, 16 November, 2018 (pp. 55-71). Springer
Open this publication in new window or tab >>Formal Verification of Random Forests in Safety-Critical Applications
2019 (English)In: Formal Techniques for Safety-Critical Systems, Springer, 2019, p. 55-71Conference paper, Published paper (Refereed)
Abstract [en]

Recent advances in machine learning and artificial intelligence are now being applied in safety-critical autonomous systems where software defects may cause severe harm to humans and the environment. Design organizations in these domains are currently unable to provide convincing arguments that systems using complex software implemented using machine learning algorithms are safe and correct.

In this paper, we present an efficient method to extract equivalence classes from decision trees and random forests, and to formally verify that their input/output mappings comply with requirements. We implement the method in our tool VoRF (Verifier of Random Forests), and evaluate its scalability on two case studies found in the literature. We demonstrate that our method is practical for random forests trained on low-dimensional data with up to 25 decision trees, each with a tree depth of 20. Our work also demonstrates the limitations of the method with high-dimensional data and touches upon the trade-off between large number of trees and time taken for verification.

Place, publisher, year, edition, pages
Springer, 2019
Series
Communications in Computer and Information Science, ISSN 1865-0929 ; 008
Keywords
Machine learning, Formal verification, Random forest, Decision tree
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-154368 (URN)10.1007/978-3-030-12988-0_4 (DOI)978-3-030-12987-3 (ISBN)978-3-030-12988-0 (ISBN)
Conference
Sixth International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2018), Gold Coast, Australia, 16 November, 2018
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2019-02-07 Created: 2019-02-07 Last updated: 2019-02-15Bibliographically approved
Bergman, S., Asplund, M. & Nadjm-Tehrani, S. (2019). Permissioned Blockchains and Distributed Databases: A Performance Study. Concurrency and Computation
Open this publication in new window or tab >>Permissioned Blockchains and Distributed Databases: A Performance Study
2019 (English)In: Concurrency and Computation, ISSN 1532-0626, E-ISSN 1532-0634, Concurrency and Computation, Practice and ExperienceArticle in journal (Refereed) Epub ahead of print
Abstract [en]

Blockchains are increasingly studied in the context of new applications. Permissioned blockchains promise to deal with the issue of complete removal of trust, a notion that is currently the hallmark of the developed society. Before the idea is adopted in contexts where resource efficiency and fast operation is a requirement, one could legitimately ask the question: can permissioned blockchains match the performance of traditional large‐scale databases? This paper compares two popular frameworks, Hyperledger Fabric and Apache Cassandra, as representatives of permissioned blockchains and distributed databases, respectively. We compare their latency for varying workloads and network sizes. The results show that, for small systems, blockchains can start to compete with traditional databases, but also that the difference in consistency models and differences in setup can have a large impact on the resulting performance.

Place, publisher, year, edition, pages
John Wiley & Sons, 2019
Keywords
blockchains, Cassandra, databases, Fabric, latency
National Category
Engineering and Technology Computer Systems
Identifiers
urn:nbn:se:liu:diva-161756 (URN)10.1002/cpe.5227 (DOI)
Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2020-03-11Bibliographically approved
Almgren, M., Andersson, P., Björkman, G., Ekstedt, M., Hallberg, J., Nadjm-Tehrani, S. & Westring, E. (2019). RICS-el: Building a National Testbed for Research and Training on SCADA Security. In: Eric Luiijf, Inga Žutautaitė and Bernhard Hämmerli (Ed.), Critical Information Infrastructures Security: 13th International Conference, CRITIS 2018, Kaunas, Lithuania, September 24-26, 2018, Revised Selected Papers (pp. 219-225). Springer
Open this publication in new window or tab >>RICS-el: Building a National Testbed for Research and Training on SCADA Security
Show others...
2019 (English)In: Critical Information Infrastructures Security: 13th International Conference, CRITIS 2018, Kaunas, Lithuania, September 24-26, 2018, Revised Selected Papers / [ed] Eric Luiijf, Inga Žutautaitė and Bernhard Hämmerli, Springer, 2019, p. 219-225Chapter in book (Refereed)
Abstract [en]

Trends show that cyber attacks targeting critical infrastructures are increasing, but security research for protecting such systems are challenging. There is a gap between the somewhat simplified models researchers at universities can sustain contra the complex systems at infrastructure owners that seldom can be used for direct research. There is also a lack of common datasets for research benchmarking. This paper presents a national experimental testbed for security research within supervisory control and data acquisition systems (SCADA), accessible for both research training and experiments. The virtualized testbed has been designed and implemented with both vendor experts and security researchers to balance the goals of realism with specific research needs. It includes a real SCADA product for energy management, a number of network zones, substation nodes, and a simulated power system. This environment enables creation of scenarios similar to real world utility scenarios, attack generation, development of defence mechanisms, and perhaps just as important: generating open datasets for comparative research evaluation.

Place, publisher, year, edition, pages
Springer, 2019
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11260
Keywords
Cyber security in C(I)I systems; Modelling; Simulation Analysis and Validation approaches to C(I)IP Training for C(I)IP and effective intervention
National Category
Computer Systems
Identifiers
urn:nbn:se:liu:diva-154379 (URN)10.1007/978-3-030-05849-4_17 (DOI)9783030058487 (ISBN)9783030058494 (ISBN)9783030058494 (ISBN)
Available from: 2019-02-11 Created: 2019-02-11 Last updated: 2019-02-26Bibliographically approved
Lin, C.-Y. & Nadjm-Tehrani, S. (2019). Timing Patterns and Correlations in Spontaneous SCADA Traffic for Anomaly Detection. In: : 22nd International Symposium on Research on Attacks, Intrusions, and Defenses (RAID). Paper presented at 22nd International Symposium on Research on Attacks, Intrusions, and Defenses (RAID), Beijing, China, September 23-25, 2019. USENIX - The Advanced Computing Systems Association
Open this publication in new window or tab >>Timing Patterns and Correlations in Spontaneous SCADA Traffic for Anomaly Detection
2019 (English)In: : 22nd International Symposium on Research on Attacks, Intrusions, and Defenses (RAID), USENIX - The Advanced Computing Systems Association, 2019Conference paper, Published paper (Refereed)
Abstract [en]

Supervisory Control and Data Acquisition (SCADA) systems operate critical infrastructures in our modern society despite their vulnerability to attacks and misuse. There are several anomaly detection systems based on the cycles of polling mechanisms used in SCADA systems, but the feasibility of anomaly detection systems based on non-polling traffic, so called spontaneous events, is not well-studied. This paper presents a novel approach to modeling the timing characteristics of spontaneous events in an IEC-60870-5-104 network and exploits the model for anomaly detection. The system is tested with a dataset from a real power utility with injected timing effects from two attack scenarios. One attack causes timing anomalies due to persistent malfunctioning in the field devices, and the other generates intermittent anomalies caused by malware on the field devices, which is considered as stealthy. The detection accuracy and timing performance are promising for all the experiments with persistent anomalies. With intermittent anomalies, we found that our approach is effective for anomalies in low-volume traffic or attacks lasting over 1 hour.

Place, publisher, year, edition, pages
USENIX - The Advanced Computing Systems Association, 2019
Keywords
Anomaly detection, SCADA systems, IEC-60870-5-104, Critical infrastructure
National Category
Computer Engineering
Identifiers
urn:nbn:se:liu:diva-161757 (URN)
Conference
22nd International Symposium on Research on Attacks, Intrusions, and Defenses (RAID), Beijing, China, September 23-25, 2019
Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2019-11-18Bibliographically approved
Toczé, K., Schmitt, N., Brandic, I., Aral, A. & Nadjm-Tehrani, S. (2019). Towards Edge Benchmarking: A Methodology for Characterizing Edge Workloads. In: Proceedings of 4th International Workshop on Foundations and Applications of Self* Systems (FAS*W),: . Paper presented at 4th International Workshop on Foundations and Applications of Self* Systems (FAS*W), Umea, Sweden, 16-20 June 2019 (pp. 70-71). IEEE
Open this publication in new window or tab >>Towards Edge Benchmarking: A Methodology for Characterizing Edge Workloads
Show others...
2019 (English)In: Proceedings of 4th International Workshop on Foundations and Applications of Self* Systems (FAS*W),, IEEE, 2019, p. 70-71Conference paper, Published paper (Refereed)
Abstract [en]

The edge computing paradigm has recently attracted research efforts coming from different application domains. However, evaluating an edge platform or algorithm is impeded by the lack of suitable benchmarks. We propose a methodology for characterizing edge workloads from different application domains. It is a first step towards defining workloads to be included in a future edge benchmarking suite. We evaluate the methodology on three use cases and find that defining a common and standard set of workloads is plausible.

Place, publisher, year, edition, pages
IEEE, 2019
National Category
Computer Systems
Identifiers
urn:nbn:se:liu:diva-161760 (URN)10.1109/FAS-W.2019.00030 (DOI)000518905900017 ()2-s2.0-85071474510 (Scopus ID)978-1-7281-2406-3 (ISBN)
Conference
4th International Workshop on Foundations and Applications of Self* Systems (FAS*W), Umea, Sweden, 16-20 June 2019
Note

Funding agencies:  Swedish national graduate school in computer science (CUGS)

Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2020-03-29Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-1485-0802

Search in DiVA

Show all publications