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

Direct link
Nadjm-Tehrani, SiminORCID iD iconorcid.org/0000-0002-1485-0802
Alternative names
Publications (10 of 134) Show all publications
Colaco, V. & Nadjm-Tehrani, S. (2023). Formal Verification of Tree Ensembles against Real-World Composite Geometric Perturbations. In: Proceedings of the Workshop on Artificial Intelligence Safety 2023 (SafeAI 2023) co-located with the Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI 2023): . Paper presented at The AAAI-23 Workshop on Artificial Intelligence Safety (SafeAI 2023), Washington DC, USA, February 13-14, 2023. CEUR-WS, 3381, Article ID 38.
Open this publication in new window or tab >>Formal Verification of Tree Ensembles against Real-World Composite Geometric Perturbations
2023 (English)In: Proceedings of the Workshop on Artificial Intelligence Safety 2023 (SafeAI 2023) co-located with the Thirty-Seventh AAAI Conference on Artificial Intelligence (AAAI 2023), CEUR-WS , 2023, Vol. 3381, article id 38Conference paper, Published paper (Refereed)
Abstract [en]

Since machine learning components are now being considered for integration in safety-critical systems, safety stakeholdersshould be able to provide convincing arguments that the systems are safe for use in realistic deployment settings. In the caseof vision-based systems, the use of tree ensembles calls for formal stability verification against a host of composite geometricperturbations that the system may encounter. Such perturbations are a combination of an affine transformation like rotation,scaling, or translation and a pixel-wise transformation like changes in lighting. However, existing verification approachesmostly target small norm-based perturbations, and do not account for composite geometric perturbations. In this work,we present a novel method to precisely define the desired stability regions for these types of perturbations. We propose afeature space modelling process that generates abstract intervals which can be passed to VoTE, an efficient formal verificationengine that is specialised for tree ensembles. Our method is implemented as an extension to VoTE by defining a new propertychecker. The applicability of the method is demonstrated by verifying classifier stability and computing metrics associatedwith stability and correctness, i.e., robustness, fragility, vulnerability, and breakage, in two case studies. In both case studies,targeted data augmentation pre-processing steps were applied for robust model training. Our results show that even modelstrained with augmented data are unable to handle these types of perturbations, thereby emphasising the need for certifiedrobust training for tree ensembles.

Place, publisher, year, edition, pages
CEUR-WS, 2023
Series
CEUR Workshop Proceedings, ISSN 1613-0073 ; 3381
Keywords
Machine Learning, Formal Verification, Tree Ensembles, Composite Perturbations, Geometric Perturbations, Random Forests, Gradient Boosting Machines, Semantic Perturbations, Stability, Robustness, Trustworthy AI, Trustworthy Computing
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-195996 (URN)
Conference
The AAAI-23 Workshop on Artificial Intelligence Safety (SafeAI 2023), Washington DC, USA, February 13-14, 2023
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Available from: 2023-06-30 Created: 2023-06-30 Last updated: 2023-07-06Bibliographically approved
Lin, C.-Y. & Nadjm-Tehrani, S. (2021). A Comparative Analysis of Emulated and Real IEC-104 Spontaneous Traffic in Power System Networks. In: Abie, Habtamu; Ranise, Silvio; Verderame, Luca; Cambiaso, Enrico; Ugarelli, Rita; Giunta, Gabriele; Praça, Isabel; Battisti, Federica (Ed.), Cyber-Physical Security for Critical Infrastructures Protection: . Paper presented at International Workshop on Cyber-Physical Security for Critical Infrastructures Protection (pp. 207-223). Springer International Publishing
Open this publication in new window or tab >>A Comparative Analysis of Emulated and Real IEC-104 Spontaneous Traffic in Power System Networks
2021 (English)In: Cyber-Physical Security for Critical Infrastructures Protection / [ed] Abie, Habtamu; Ranise, Silvio; Verderame, Luca; Cambiaso, Enrico; Ugarelli, Rita; Giunta, Gabriele; Praça, Isabel; Battisti, Federica, Springer International Publishing , 2021, p. 207-223Conference paper, Published paper (Refereed)
Abstract [en]

Supervisory and Data Acquisition (SCADA) systems control and monitor modern power networks. As attacks targeting SCADA systems are increasing, significant research is conducted to defend SCADA networks including variations of anomaly detection. Due to the sensitivity of real data, many defence mechanisms have been tested only in small testbeds or emulated traffic that were designed with assumptions on how SCADA systems behave. This work provides a timing characterization of IEC-104 spontaneous traffic and compares the results from emulated traffic and real traffic to verify if the network characteristics appearing in testbeds and emulated traffic coincide with real traffic. Among three verified characteristics, two of them appear in the real dataset but in a less regular way, and one does not appear in the collected real data. The insights from these observations are discussed in terms of presumed differences between emulated and real traffic and how those differences are generated.

Place, publisher, year, edition, pages
Springer International Publishing, 2021
Keywords
SCADA, Traffic characterization, IEC-104, Timing analysis
National Category
Computer Engineering
Identifiers
urn:nbn:se:liu:diva-189696 (URN)10.1007/978-3-030-69781-5_14 (DOI)9783030697808 (ISBN)9783030697815 (ISBN)
Conference
International Workshop on Cyber-Physical Security for Critical Infrastructures Protection
Funder
Swedish Civil Contingencies Agency
Available from: 2022-11-03 Created: 2022-11-03 Last updated: 2022-11-03
Toczé, K. & Nadjm-Tehrani, S. (2021). Corrigendum to “A Taxonomy for Management and Optimization of Multiple Resources in Edge Computing” (vol 2018, 7476201, 2018). Wireless Communications & Mobile Computing, 2021, Article ID 9876126.
Open this publication in new window or tab >>Corrigendum to “A Taxonomy for Management and Optimization of Multiple Resources in Edge Computing” (vol 2018, 7476201, 2018)
2021 (English)In: Wireless Communications & Mobile Computing, ISSN 1530-8669, E-ISSN 1530-8677, Vol. 2021, article id 9876126Article in journal (Other academic) Published
Abstract [en]

n/a

Place, publisher, year, edition, pages
Wiley Hindawi, 2021
National Category
Communication Systems
Identifiers
urn:nbn:se:liu:diva-184115 (URN)10.1155/2021/9876126 (DOI)000770932000008 ()
Available from: 2022-04-11 Created: 2022-04-11 Last updated: 2022-06-20
Lin, C.-Y., Fundin, A., Westring, E., Gustafsson, T. & Nadjm-Tehrani, S. (2021). RICSel21 Data Collection: Attacks in a Virtual Power Network. In: 2021 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm): . Paper presented at IEEE International Conference on Smart Grid Communications (SmartGridComm), Aachen, Germany, 25-28 October, 2021 (pp. 201-206). Institute of Electrical and Electronics Engineers (IEEE)
Open this publication in new window or tab >>RICSel21 Data Collection: Attacks in a Virtual Power Network
Show others...
2021 (English)In: 2021 IEEE International Conference on Communications, Control, and Computing Technologies for Smart Grids (SmartGridComm), Institute of Electrical and Electronics Engineers (IEEE), 2021, p. 201-206Conference paper, Published paper (Refereed)
Abstract [en]

Attacks against Supervisory Control and Data Acquisition (SCADA) systems operating critical infrastructures have increased since the appearance of Stuxnet. To defend critical infrastructures, security researchers need realistic datasets to evaluate and benchmark their defense mechanisms such as Anomaly Detection Systems (ADS). However, real-world data collected from critical infrastructures are too sensitive to share openly. Therefore, testbed datasets have become a viable option to balance the requirement of openness and realism. This study provides a data generation framework based on a virtual testbed with a commercial SCADA system and presents an openly available dataset called RICSel21, with packets in IEC-60870-5-104 protocol streams. The dataset is the result of performing 12 attacks, identifying the impact of attacks on a power management system and recording the logs of the seven successful attacks.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2021
Keywords
Computers, Protocols, Computer worms, Power system management, Conferences, SCADA systems, Benchmark testing
National Category
Computer Systems
Identifiers
urn:nbn:se:liu:diva-189699 (URN)10.1109/SmartGridComm51999.2021.9632328 (DOI)2-s2.0-85123913802 (Scopus ID)9781665430449 (ISBN)9781665415026 (ISBN)
Conference
IEEE International Conference on Smart Grid Communications (SmartGridComm), Aachen, Germany, 25-28 October, 2021
Funder
Swedish Civil Contingencies Agency
Available from: 2022-11-03 Created: 2022-11-03 Last updated: 2022-11-09Bibliographically approved
Toczé, K., Lindqvist, J. & Nadjm-Tehrani, S. (2020). Characterization and modeling of an edge computing mixed reality workload. Journal of Cloud Computing: Advances, Systems and Applications, 9(1), Article ID 46.
Open this publication in new window or tab >>Characterization and modeling of an edge computing mixed reality workload
2020 (English)In: Journal of Cloud Computing: Advances, Systems and Applications, E-ISSN 2192-113X, Vol. 9, no 1, article id 46Article in journal (Refereed) Published
Abstract [en]

The edge computing paradigm comes with a promise of lower application latency compared to the cloud. Moreover, offloading user device computations to the edge enables running demanding applications on resource-constrained mobile end devices. However, there is a lack of workload models specific to edge offloading using applications as their basis.In this work, we build upon the reconfigurable open-source mixed reality (MR) framework MR-Leo as a vehicle to study resource utilisation and quality of service for a time-critical mobile application that would have to rely on the edge to be widely deployed. We perform experiments to aid estimating the resource footprint and the generated load by MR-Leo, and propose an application model and a statistical workload model for it. The idea is that such empirically-driven models can be the basis of evaluations of edge algorithms within simulation or analytical studies.A comparison with a workload model used in a recent work shows that the computational demand of MR-Leo exhibits very different characteristics from those assumed for MR applications earlier.

Place, publisher, year, edition, pages
Springer, 2020
Keywords
Edge; fog computing; Mixed reality; Open-source; Empirical performance evaluation; Workload characterization and modeling; Application instrumentation for data collection; Resource footprint
National Category
Computer Sciences
Identifiers
urn:nbn:se:liu:diva-169226 (URN)10.1186/s13677-020-00190-x (DOI)000560710500001 ()2-s2.0-85089493866 (Scopus ID)
Note

Funding Agencies|Swedish National Graduate School in Computer Science (CUGS)

Available from: 2020-09-12 Created: 2020-09-12 Last updated: 2023-11-15Bibliographically approved
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)000528192400002 ()
Funder
Wallenberg AI, Autonomous Systems and Software Program (WASP)
Note

Funding agencies: Wallenberg AI, Autonomous Systems and Software Program (WASP) - Knut and Alice Wallenberg Foundation

Available from: 2020-03-24 Created: 2020-03-24 Last updated: 2022-03-19
Bergman, S., Asplund, M. & Nadjm-Tehrani, S. (2020). Permissioned Blockchains and Distributed Databases: A Performance Study. Concurrency and Computation, 32(12), Article ID e5227.
Open this publication in new window or tab >>Permissioned Blockchains and Distributed Databases: A Performance Study
2020 (English)In: Concurrency and Computation, ISSN 1532-0626, E-ISSN 1532-0634, Concurrency and Computation, Practice and Experience, Vol. 32, no 12, article id e5227Article in journal (Refereed) Published
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, 2020
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)000529224600004 ()
Available from: 2019-11-08 Created: 2019-11-08 Last updated: 2020-09-18Bibliographically approved
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
Saar de Moraes, R. & Nadjm-Tehrani, S. (2020). Verifying Resource Adequacy of Networked IMA Systems at Concept Level. In: Hasan, O. and Mallet, F. (Ed.), Formal Techniques for Safety-Critical Systems: . Paper presented at Formal Techniques for Safety-Critical Systems (FTSCS), Shenzhen, China, November 9, 2019 (pp. 40-56). Cham: Springer
Open this publication in new window or tab >>Verifying Resource Adequacy of Networked IMA Systems at Concept Level
2020 (English)In: Formal Techniques for Safety-Critical Systems / [ed] Hasan, O. and Mallet, F., Cham: Springer, 2020, p. 40-56Conference paper, Published paper (Refereed)
Abstract [en]

Complex cyber-physical systems can be difficult to analyze for resource adequacy at the concept development stage since relevant models are hard to create. During this period, details about the functions to be executed or the platforms in the architecture are partially unknown. This is especially true for Integrated Modular Avionics (IMA) Systems, for which life-cycles span over several decades, with potential changes to functionality in the future. To support the engineers evaluating conceptual designs there is a need for tools that model resources of interest in an abstract manner and allow analyses of changing architectures in a modular and scalable way. This work presents a generic timed automata-based model of a networked IMA system abstracting complex networking and computational elements of an architecture, but representing the communication needs of each application function using UPPAAL templates. The proposed model is flexible and can be modified/extended to represent different types of network topologies and communication patterns. More specifically, the different components of the IMA network, Core Processing Modules, Network End-Systems, and Switches, are represented by different templates. The templates are then instantiated to represent a conceptual design, and fed into a model checker to verify that a given platform instance supports the desired system functions in terms of network bandwidth and buffer size adequacy - in particular, whether messages can reach their final destination on time. The work identifies the limits of the tool used for this evaluation, but the conceptual model can be carried over to other tools for further studies.

Place, publisher, year, edition, pages
Cham: Springer, 2020
Series
Communications in Computer and Information Science, ISSN 1865-0929 ; 1165
Keywords
Timed automata, UPPAAL, IMA system, Concept analysis, Network resource adequacy
National Category
Computer Engineering
Identifiers
urn:nbn:se:liu:diva-170069 (URN)10.1007/978-3-030-46902-3_3 (DOI)978-3-030-46901-6 (ISBN)
Conference
Formal Techniques for Safety-Critical Systems (FTSCS), Shenzhen, China, November 9, 2019
Projects
NFFP7, project CLASSICS (NFFP7-04890)
Funder
Vinnova, NFFP7-04890
Available from: 2020-09-28 Created: 2020-09-28 Last updated: 2021-06-16Bibliographically approved
Periera, D. P., Hirata, C. & Nadjm-Tehrani, S. (2019). A STAMP-based ontology approach to support safety and security analyses. 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 analyses
2019 (English)In: Journal of Information Security and Applications, ISSN 2214-2134, E-ISSN 2214-2126, 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
Keywords
Safety assessment; Security assessment; Security ontology; STAMP/STPA-Sec
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)
Note

Funding Agencies|CNPq [403921/2016-3, 306186/2018-7]; CISB SAAB [04/2016]; national projects on aeronautics [NFFP7-04890]; research centre on Resilient Information and Control Systems

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

Search in DiVA

Show all publications