https://www.mdu.se/

mdu.sePublications
Change search
Link to record
Permanent link

Direct link
Sirjani, Marjan
Publications (10 of 56) Show all publications
Khosravi, R., Khamespanah, E., Ghassemi, F. & Sirjani, M. (2024). Actors Upgraded for Variability, Adaptability, and Determinism. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): (pp. 226-260). Springer Science and Business Media Deutschland GmbH, 14360 LNCS
Open this publication in new window or tab >>Actors Upgraded for Variability, Adaptability, and Determinism
2024 (English)In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Science and Business Media Deutschland GmbH , 2024, Vol. 14360 LNCS, p. 226-260Chapter in book (Other academic)
Abstract [en]

The Rebeca modeling language is designed as an imperative actor-based language with the goal of providing an easy-to-use language for modeling concurrent and distributed systems, with formal verification support. Rebeca has been extended to support time and probability. We extend Rebeca further with inheritance, polymorphism, interface declaration, and annotation mechanisms. These features allow us to handle variability within the model, support non-disruptive model evolution, and define method priorities. This enables Rebeca to be used more effectively in different domains, like in Software Product Lines, and holistic analysis of Cyber-Physical Systems. We develop specialized analysis techniques to support these extensions, partly integrated into Afra, the model checking tool of Rebeca.

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2024
Keywords
Actor Languages, Cyber-Physical Systems, Model Checking, Variability Modeling, Cyber Physical System, Embedded systems, Modeling languages, Software design, Actor language, Concurrent and distributed systems, Cybe-physical systems, Different domains, Interface declaration, Model evolution, Models checking, Support time
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-66094 (URN)10.1007/978-3-031-51060-1_9 (DOI)2-s2.0-85184279424 (Scopus ID)
Available from: 2024-02-20 Created: 2024-02-20 Last updated: 2024-02-20Bibliographically approved
Moradi, F., Abbaspour Asadollah, S., Pourvatan, B., Moezkarimi, Z. & Sirjani, M. (2024). CRYSTAL framework: Cybersecurity assurance for cyber-physical systems. The Journal of logical and algebraic methods in programming, 139
Open this publication in new window or tab >>CRYSTAL framework: Cybersecurity assurance for cyber-physical systems
Show others...
2024 (English)In: The Journal of logical and algebraic methods in programming, ISSN 2352-2208, E-ISSN 2352-2216, ISSN 2352-2208, Vol. 139Article in journal (Refereed) Published
Abstract [en]

We propose CRYSTAL framework for automated cybersecurity assurance of cyber-physical systems (CPS) at design-time and runtime. We build attack models and apply formal verification to recognize potential attacks that may lead to security violations. We focus on both communication and computation in designing the attack models. We build a monitor to check and manage security at runtime and use a reference model, called Tiny Digital Twin, in detecting attacks. The Tiny Digital Twin is an abstract behavioral model that is automatically derived from the state space generated by model checking during design-time. Using CRYSTAL, we are able to systematically model and check complex coordinated attacks. In this paper we discuss the applicability of CRYSTAL in security analysis and attack detection for different case studies, Temperature Control System (TCS), Pneumatic Control System (PCS), and Secure Water Treatment System (SWaT). We provide a detailed description of the framework and explain how it works in different cases.

Place, publisher, year, edition, pages
Elsevier, 2024
Keywords
Cyber-Physical Systems (CPS), Formal verification, Model abstraction, Attack detection system, Runtime monitoring, Tiny Digital Twin
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-66419 (URN)10.1016/j.jlamp.2024.100965 (DOI)2-s2.0-85189706631 (Scopus ID)
Available from: 2024-04-14 Created: 2024-04-14 Last updated: 2024-04-17Bibliographically approved
Johansson, B., Pourvatan, B., Moezkarimi, Z., Papadopoulos, A. & Sirjani, M. (2024). Formal Verification of Consistency for Systems with Redundant Controllers. In: Electronic Proceedings in Theoretical Computer Science, EPTCS: . Paper presented at 6th Workshop on Models for Formal Analysis of Real Systems, MARS 2024, Luxembourg City, 6 April 2024 (pp. 169-191). Open Publishing Association, 399
Open this publication in new window or tab >>Formal Verification of Consistency for Systems with Redundant Controllers
Show others...
2024 (English)In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2024, Vol. 399, p. 169-191Conference paper, Published paper (Refereed)
Abstract [en]

A potential problem that may arise in the domain of distributed control systems is the existence of more than one primary controller in redundancy plans that may lead to inconsistency. An algorithm called NRP FD is proposed to solve this issue by prioritizing consistency over availability. In this paper, we demonstrate how by using modeling and formal verification, we discovered an issue in NRP FD where we may have two primary controllers at the same time. We then provide a solution to mitigate the identified issue, thereby enhancing the robustness and reliability of such systems.

Place, publisher, year, edition, pages
Open Publishing Association, 2024
Keywords
Controllers, Distributed parameter control systems, Finite difference method, Potential problems, Redundant controllers, Formal verification
National Category
Electrical Engineering, Electronic Engineering, Information Engineering
Identifiers
urn:nbn:se:mdh:diva-66500 (URN)10.4204/EPTCS.399.8 (DOI)2-s2.0-85190277600 (Scopus ID)
Conference
6th Workshop on Models for Formal Analysis of Real Systems, MARS 2024, Luxembourg City, 6 April 2024
Note

Conference code: 198553

Available from: 2024-04-25 Created: 2024-04-25 Last updated: 2024-04-25Bibliographically approved
Moradi, F., Pourvatan, B., Abbaspour Asadollah, S. & Sirjani, M. (2024). Tiny Twins for detecting cyber-attacks at runtime using concise Rebeca time transition system. Journal of Parallel and Distributed Computing, 184, Article ID 104780.
Open this publication in new window or tab >>Tiny Twins for detecting cyber-attacks at runtime using concise Rebeca time transition system
2024 (English)In: Journal of Parallel and Distributed Computing, ISSN 0743-7315, E-ISSN 1096-0848, Vol. 184, article id 104780Article in journal (Refereed) Published
Abstract [en]

This paper presents a method for detecting cyber-attacks in cyber-physical systems using a monitor. The method employs an abstract model called Tiny Twin, which is built at design time and is used at runtime to detect inconsistencies. Tiny Twin is a state transition system that represents the observable behavior of the system from the monitor point of view. We model the behavior of the system in the Rebeca modeling language and use Afra model checker to generate the state space. The Tiny Twin is built automatically, by abstracting the state space while keeping the observable actions and preserving the trace equivalence. For doing that we had to solve the complexities in the state space introduced by time-shifts, nondeterministic assignments and abstraction of internal actions. We formally define the state space as Concise Rebeca Timed Transition System (CRTTS), and then map CRTTS to an LTS. The LTS is then fed to a tool to abstract away the non-observable actions.

Place, publisher, year, edition, pages
Academic Press Inc., 2024
Keywords
Cyber-security, Intrusion detection systems, Model abstraction, Model checking, Runtime monitoring, Abstracting, Computer crime, Crime, Cyber attacks, Cyber Physical System, Embedded systems, Intrusion detection, Modeling languages, Network security, Cyber security, Cyber-attacks, Models checking, Runtimes, State-space, Time transition, Timed transition systems
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-64590 (URN)10.1016/j.jpdc.2023.104780 (DOI)001099111600001 ()2-s2.0-85173631477 (Scopus ID)
Available from: 2023-10-30 Created: 2023-10-30 Last updated: 2024-04-14Bibliographically approved
Marksteiner, S., Sirjani, M. & Sjödin, M. (2024). Using Automata Learning for Compliance Evaluation of Communication Protocols on an NFC Handshake Example. In: Lecture Notes in Computer Science: . Paper presented at 8th International Conference on Engineering of Computer-Based Systems, ECBS 2023, Västerås, 16 October 2023 through 18 October 2023 (pp. 170-190). Springer Science and Business Media Deutschland GmbH
Open this publication in new window or tab >>Using Automata Learning for Compliance Evaluation of Communication Protocols on an NFC Handshake Example
2024 (English)In: Lecture Notes in Computer Science, Springer Science and Business Media Deutschland GmbH , 2024, p. 170-190Conference paper, Published paper (Refereed)
Abstract [en]

Near-Field Communication (NFC) is a widely adopted standard for embedded low-power devices in very close proximity. In order to ensure a correct system, it has to comply to the ISO/IEC 14443 standard. This paper concentrates on the low-level part of the protocol (ISO/IEC 14443-3) and presents a method and a practical implementation that complements traditional conformance testing. We infer a Mealy state machine of the system-under-test using active automata learning. This automaton is checked for bisimulation with a specification automaton modelled after the standard, which provides a strong verdict of conformance or non-conformance. As a by-product, we share some observations of the performance of different learning algorithms and calibrations in the specific setting of ISO/IEC 14443-3, which is the difficulty to learn models of system that a) consist of two very similar structures and b) very frequently give no answer (i.e. a timeout as an output).

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14390 LNCS
Keywords
Automata Learning, Bisimulation, Formal Methods, NFC, Protocol Compliance, Automata theory, ISO Standards, Learning algorithms, Learning systems, Near field communication, Automaton learning, Bisimulations, Close proximity, Communications protocols, Compliance evaluations, Conformance testing, ISO/IEC-14443, Low-power devices, Near-field communication
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-65246 (URN)10.1007/978-3-031-49252-5_13 (DOI)2-s2.0-85180149916 (Scopus ID)9783031492518 (ISBN)
Conference
8th International Conference on Engineering of Computer-Based Systems, ECBS 2023, Västerås, 16 October 2023 through 18 October 2023
Available from: 2024-01-03 Created: 2024-01-03 Last updated: 2024-03-01Bibliographically approved
Khamespanah, E., Sirjani, M. & Khosravi, R. (2023). Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family Models. In: Lect. Notes Comput. Sci.: . Paper presented at Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 72-87). Springer Science and Business Media Deutschland GmbH
Open this publication in new window or tab >>Afra: An Eclipse-Based Tool with Extensible Architecture for Modeling and Model Checking of Rebeca Family Models
2023 (English)In: Lect. Notes Comput. Sci., Springer Science and Business Media Deutschland GmbH , 2023, p. 72-87Conference paper, Published paper (Refereed)
Abstract [en]

Afra is an Eclipse-based tool for the modeling and model checking of Rebeca family models. Together with the standard enriched editor, easy to trace counter-example viewer, modular temporal property definition, exporting a model and its transition system to some other formats facilities are features of Afra. Rebeca family provides actor-based modeling languages which are designed to bridge the gap between formal methods and software engineering. Faithfulness to the system being modeled, and the usability of Rebeca family languages help in ease of modeling and analysis of the model, together with the synthesis of the system based on the model. In this paper, architectural decisions and design strategies we made in the development of Afra are presented. This makes Afra an extensible and reusable application for the modeling and analysis of Rebeca family models. Here, we show how different compilers can be developed for the family of languages which are the same in general language constructs but have some minor differences. Then we show how the model checking engine for these different languages is designed. Despite the fact that Afra has a layered object-oriented design and is developed in Java technology, we use C++ codes for developing its model checking for the performance purposes. This decision made the design of the application even harder.

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2023
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14155 LNCS
Keywords
Actors, Afra, Eclipse, Model Checking, Rebeca, Bridges, C++ (programming language), Computer software reusability, Formal methods, Modeling languages, Object oriented programming, Actor, Counter examples, Modeling checking, Modelling and analysis, Models checking, Modulars, Rebecum, Temporal property
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-64449 (URN)10.1007/978-3-031-42441-0_6 (DOI)2-s2.0-85171563334 (Scopus ID)9783031424403 (ISBN)
Conference
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Available from: 2023-10-05 Created: 2023-10-05 Last updated: 2023-10-05Bibliographically approved
Marksteiner, S., Schmittner, C., Christl, K., Nickovic, D., Sjödin, M. & Sirjani, M. (2023). From TARA to Test: Automated Automotive Cybersecurity Test Generation Out of Threat Modeling. In: Proceedings: CSCS 2023 - 7th ACM Computer Science in Cars Symposium: . Paper presented at 7th ACM Computer Science in Cars Symposium, CSCS 2023, Darmstadt, 5 December 2023. Association for Computing Machinery, Inc
Open this publication in new window or tab >>From TARA to Test: Automated Automotive Cybersecurity Test Generation Out of Threat Modeling
Show others...
2023 (English)In: Proceedings: CSCS 2023 - 7th ACM Computer Science in Cars Symposium, Association for Computing Machinery, Inc , 2023Conference paper, Published paper (Refereed)
Abstract [en]

The United Nations Economic Commission for Europe (UNECE) demands the management of cyber security risks in vehicle design and that the effectiveness of these measures is verified by testing. Generally, with rising complexity and openness of systems via software-defined vehicles, verification through testing becomes a very important for security assurance. This mandates the introduction of industrial-grade cybersecurity testing in automotive development processes. Currently, the automotive cybersecurity testing procedures are not specified or automated enough to be able to deliver tests in the amount and thoroughness needed to keep up with that regulation, let alone doing so in a cost-efficient manner. This paper presents a methodology to automatically generate technology-agnostic test scenarios from the results of threat analysis and risk assessment (TARA) process. Our approach is to transfer the resulting threat models into attack trees and label their edges using actions from a domain-specific language (DSL) for attack descriptions. This results in a labelled transitions system (LTS), in which every labelled path intrinsically forms a test scenario. In addition, we include the concept of Cybersecurity Assurance Levels (CALs) and Targeted Attack Feasibility (TAF) into testing by assigning them as costs to the attack path. This abstract test scenario can be compiled into a concrete test case by augmenting it with implementation details. Therefore, the efficacy of the measures taken because of the TARA can be verified and documented. As TARA is a de-facto mandatory step in the UNECE regulation and the relevant ISO standard, automatic test generation (also mandatory) out of it could mean a significant improvement in efficiency, as two steps could be done at once.

Place, publisher, year, edition, pages
Association for Computing Machinery, Inc, 2023
Keywords
Automotive, CAL, Cybersecurity, Life Cycle, TAF, Testing
National Category
Computer Systems
Identifiers
urn:nbn:se:mdh:diva-65679 (URN)10.1145/3631204.3631864 (DOI)001150368200005 ()2-s2.0-85182016784 (Scopus ID)9798400704543 (ISBN)
Conference
7th ACM Computer Science in Cars Symposium, CSCS 2023, Darmstadt, 5 December 2023
Available from: 2024-01-24 Created: 2024-01-24 Last updated: 2024-03-01Bibliographically approved
Salimi, M., Loni, M. & Sirjani, M. (2023). Learning Activation Functions for Adversarial Attack Resilience in CNNs. In: Lect. Notes Comput. Sci.: . Paper presented at Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 203-214). Springer Science and Business Media Deutschland GmbH
Open this publication in new window or tab >>Learning Activation Functions for Adversarial Attack Resilience in CNNs
2023 (English)In: Lect. Notes Comput. Sci., Springer Science and Business Media Deutschland GmbH , 2023, p. 203-214Conference paper, Published paper (Refereed)
Abstract [en]

Adversarial attacks on convolutional neural networks (CNNs) have been a serious concern in recent years, as they can cause CNNs to produce inaccurate predictions. Through our analysis of training CNNs with adversarial examples, we discovered that this was primarily caused by naïvely selecting ReLU as the default choice for activation functions. In contrast to the focus of recent works on proposing adversarial training methods, we study the feasibility of an innovative alternative: learning novel activation functions to make CNNs more resilient to adversarial attacks. In this paper, we propose a search framework that combines simulated annealing and late acceptance hill-climbing to find activation functions that are more robust against adversarial attacks in CNN architectures. The proposed search method has superior search convergence compared to commonly used baselines. The proposed method improves the resilience to adversarial attacks by achieving up to 17.1%, 22.8%, and 16.6% higher accuracy against BIM, FGSM, and PGD attacks, respectively, over ResNet-18 trained on the CIFAR-10 dataset.

Place, publisher, year, edition, pages
Springer Science and Business Media Deutschland GmbH, 2023
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14125 LNAI
Keywords
Activation Function, Adversarial Attack, Convolutional Neural Network, Robustness, Activation analysis, Chemical activation, Convolution, Convolutional neural networks, Activation functions, Attack resiliences, High-accuracy, Hill climbing, Neural network architecture, Search method, Training methods, Simulated annealing
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-64441 (URN)10.1007/978-3-031-42505-9_18 (DOI)2-s2.0-85172420687 (Scopus ID)9783031425042 (ISBN)
Conference
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Available from: 2023-10-05 Created: 2023-10-05 Last updated: 2023-10-05Bibliographically approved
Ebrahimi, E., Khamespanah, E., Sirjani, M. & Mohammadi, S. (2023). Model Checking of Hyperledger Fabric Smart Contracts. In: IEEE Int. Conf. Emerging Technol. Factory Autom., ETFA: . Paper presented at IEEE International Conference on Emerging Technologies and Factory Automation, ETFA. Institute of Electrical and Electronics Engineers Inc.
Open this publication in new window or tab >>Model Checking of Hyperledger Fabric Smart Contracts
2023 (English)In: IEEE Int. Conf. Emerging Technol. Factory Autom., ETFA, Institute of Electrical and Electronics Engineers Inc. , 2023Conference paper, Published paper (Refereed)
Abstract [en]

Conducting interactions between shared-purpose organizations that are not entirely trustworthy of each other without centralized oversight is an idea that emerged with the advent of private blockchains such as Hyperledger Fabric and its smart contracts. It is critical to check contracts to ensure their proper functionality, as organizations may collaborate with competitors. Due to the new architecture of Hyperledger Fabric, tools in this area are limited. To formally verify the source code of contracts, we mapped Fabric contract concepts into the Rebeca modeling language. Rebeca is an actor-based language that enables the modeling of concurrent and distributed systems and is supported by a model checking tool, Afra. We have identified vulnerabilities such as deadlock and starvation by examining the desired properties. Using the model checking approach, we could debug the code and hence benefit from speeding up the transactions, creating fewer extra blocks, requiring less storage space to store the ledger, and avoiding wasting computing resources.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers Inc., 2023
Keywords
Hyperledger Fabric, Model Checking, Smart Contracts, Distributed ledger, Modeling languages, Program debugging, Block-chain, Centralised, Computing resource, Concurrent and distributed systems, Hyperledg fabric, Model checking tools, Models checking, Property, Source codes, Storage spaces, Smart contract
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:mdh:diva-64703 (URN)10.1109/ETFA54631.2023.10275704 (DOI)2-s2.0-85175470217 (Scopus ID)9798350339918 (ISBN)
Conference
IEEE International Conference on Emerging Technologies and Factory Automation, ETFA
Available from: 2023-11-09 Created: 2023-11-09 Last updated: 2023-11-09Bibliographically approved
Salimi, M., Loni, M., Sirjani, M., Cicchetti, A. & Abbaspour Asadollah, S. (2023). SARAF: Searching for Adversarial Robust Activation Functions. In: ACM International Conference Proceeding Series: . Paper presented at 6th International Conference on Machine Vision and Applications, ICMVA 2023, Singapore, Singapore, 10 March 2023 through 12 March 2023 (pp. 174-182). Association for Computing Machinery
Open this publication in new window or tab >>SARAF: Searching for Adversarial Robust Activation Functions
Show others...
2023 (English)In: ACM International Conference Proceeding Series, Association for Computing Machinery , 2023, p. 174-182Conference paper, Published paper (Refereed)
Abstract [en]

Convolutional Neural Networks (CNNs) have received great attention in the computer vision domain. However, CNNs are vulnerable to adversarial attacks, which are manipulations of input data that are imperceptible to humans but can fool the network. Several studies tried to address this issue, which can be divided into two categories: (i) training the network with adversarial examples, and (ii) optimizing the network architecture and/or hyperparameters. Although adversarial training is a sufficient defense mechanism, they suffer from requiring a large volume of training samples to cover a wide perturbation bound. Tweaking network activation functions (AFs) has been shown to provide promising results where CNNs suffer from performance loss. However, optimizing network AFs for compensating the negative impacts of adversarial attacks has not been addressed in the literature. This paper proposes the idea of searching for AFs that are robust against adversarial attacks. To this aim, we leverage the Simulated Annealing (SA) algorithm with a fast convergence time. This proposed method is called SARAF. We demonstrate the consistent effectiveness of SARAF by achieving up to 16.92%, 18.3%, and 15.57% accuracy improvement against BIM, FGSM, and PGD adversarial attacks, respectively, over ResNet-18 with ReLU AFs (baseline) trained on CIFAR-10. Meanwhile, SARAF provides a significant search efficiency compared to random search as the optimization baseline.

Place, publisher, year, edition, pages
Association for Computing Machinery, 2023
Keywords
Activation Function, Adversarial Attack, Convolutional Neural Network, Optimization, Robustness, Chemical activation, Convolution, Convolutional neural networks, Network architecture, Activation functions, Defence mechanisms, Hyper-parameter, Input datas, Large volumes, Network activations, Optimisations, Simulated annealing
National Category
Computer Sciences
Identifiers
urn:nbn:se:mdh:diva-63891 (URN)10.1145/3589572.3589598 (DOI)2-s2.0-85163400963 (Scopus ID)9781450399531 (ISBN)
Conference
6th International Conference on Machine Vision and Applications, ICMVA 2023, Singapore, Singapore, 10 March 2023 through 12 March 2023
Available from: 2023-07-19 Created: 2023-07-19 Last updated: 2023-07-19Bibliographically approved
Organisations

Search in DiVA

Show all publications