Visible to the public Biblio

Filters: Keyword is Automata  [Clear All Filters]
Engram, S., Ligatti, J..  2020.  Through the Lens of Code Granularity: A Unified Approach to Security Policy Enforcement. 2020 IEEE Conference on Application, Information and Network Security (AINS). :41—46.

A common way to characterize security enforcement mechanisms is based on the time at which they operate. Mechanisms operating before a program's execution are static mechanisms, and mechanisms operating during a program's execution are dynamic mechanisms. This paper introduces a different perspective and classifies mechanisms based on the granularity of program code that they monitor. Classifying mechanisms in this way provides a unified view of security mechanisms and shows that all security mechanisms can be encoded as dynamic mechanisms that operate at different levels of program code granularity. The practicality of the approach is demonstrated through a prototype implementation of a framework for enforcing security policies at various levels of code granularity on Java bytecode applications.

Roy, P., Mazumdar, C..  2018.  Modeling of Insider Threat using Enterprise Automaton. 2018 Fifth International Conference on Emerging Applications of Information Technology (EAIT). :1—4.
Substantial portions of attacks on the security of enterprises are perpetrated by Insiders having authorized privileges. Thus insider threat and attack detection is an important aspect of Security management. In the published literature, efforts are on to model the insider threats based on the behavioral traits of employees. The psycho-social behaviors are hard to encode in the software systems. Also, in some cases, there are privacy issues involved. In this paper, the human and non-human agents in a system are described in a novel unified model. The enterprise is described as an automaton and its states are classified secure, safe, unsafe and compromised. The insider agents and threats are modeled on the basis of the automaton and the model is validated using a case study.
Wang, H., Yao, G., Wang, B..  2020.  A Quantum Concurrent Signature Scheme Based on the Quantum Finite Automata Signature Scheme. 2020 IEEE 14th International Conference on Anti-counterfeiting, Security, and Identification (ASID). :125–129.
When using digital signatures, we need to deal with the problem of fairness of information exchange. To solve this problem, Chen, etc. introduced a new conception which is named concurrent signatures in Eurocrypt'04. Using concurrent signatures scheme, two entities in the scheme can generate two ambiguous signatures until one of the entities releases additional information which is called keystone. After the keystone is released, the two ambiguous signatures will be bound to their real signers at the same time. In order to provide a method to solve the fairness problem of quantum digital signatures, we propose a new quantum concurrent signature scheme. The scheme we proposed does not use a trusted third party in a quantum computing environment, and has such advantages as no need to conduct complex quantum operations and easy to implement by a quantum circuit. Quantum concurrent signature improves the theory of quantum cryptography, and it also provides broad prospects for the specific applications of quantum cryptography.
Moormann, L., Mortel-Fronczak, J. M. van de, Fokkink, W. J., Rooda, J. E..  2020.  Exploiting Symmetry in Dependency Graphs for Model Reduction in Supervisor Synthesis. 2020 IEEE 16th International Conference on Automation Science and Engineering (CASE). :659–666.
Supervisor synthesis enables the design of supervisory controllers for large cyber-physical systems, with high guarantees for functionality and safety. The complexity of the synthesis problem, however, increases exponentially with the number of system components in the cyber-physical system and the number of models of this system, often resulting in lengthy or even unsolvable synthesis procedures. In this paper, a new method is proposed for reducing the model of the system before synthesis to decrease the required computational time and effort. The method consists of three steps for model reduction, that are mainly based on symmetry in dependency graphs of the system. Dependency graphs visualize the components in the system and the relations between these components. The proposed method is applied in a case study on the design of a supervisory controller for a road tunnel. In this case study, the model reduction steps are described, and results are shown on the effectiveness of model reduction in terms of model size and synthesis time.
Lanotte, R., Merro, M., Munteanu, A..  2020.  Runtime Enforcement for Control System Security. 2020 IEEE 33rd Computer Security Foundations Symposium (CSF). :246–261.
With the explosion of Industry 4.0, industrial facilities and critical infrastructures are transforming into “smart” systems that dynamically adapt to external events. The result is an ecosystem of heterogeneous physical and cyber components, such as programmable logic controllers, which are more and more exposed to cyber-physical attacks, i.e., security breaches in cyberspace that adversely affect the physical processes at the core of industrial control systems. We apply runtime enforcement techniques, based on an ad-hoc sub-class of Ligatti et al.'s edit automata, to enforce specification compliance in networks of potentially compromised controllers, formalised in Hennessy and Regan's Timed Process Language. We define a synthesis algorithm that, given an alphabet P of observable actions and an enforceable regular expression e capturing a timed property for controllers, returns a monitor that enforces the property e during the execution of any (potentially corrupted) controller with alphabet P and complying with the property e. Our monitors correct and suppress incorrect actions coming from corrupted controllers and emit actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical properties, such as transparency and soundness, the proposed enforcement ensures non-obvious properties, such as polynomial complexity of the synthesis, deadlock- and diverge-freedom of monitored controllers, together with scalability when dealing with networks of controllers.
Chekashev, A., Demianiuk, V., Kogan, K..  2020.  Poster: Novel Opportunities in Design of Efficient Deep Packet Inspection Engines. 2020 IEEE 28th International Conference on Network Protocols (ICNP). :1–2.
Deep Packet Inspection (DPI) is an essential building block implementing various services on data plane [5]. Usually, DPI engines are centered around efficient implementation of regular expressions both from the required memory and lookup time perspectives. In this paper, we explore and generalize original approaches used for packet classifiers [7] to regular expressions. Our preliminary results establish a promising direction for the efficient implementation of DPI engines.
Karmakar, R., Jana, S. S., Chattopadhyay, S..  2019.  A Cellular Automata Guided Obfuscation Strategy For Finite-State-Machine Synthesis. 2019 56th ACM/IEEE Design Automation Conference (DAC). :1–6.
A popular countermeasure against IP piracy relies on obfuscating the Finite State Machine (FSM), which is assumed to be the heart of a digital system. In this paper, we propose to use a special class of non-group additive cellular automata (CA) called D1 * CA, and it's counterpart D1 * CAdual to obfuscate each state-transition of an FSM. The synthesized FSM exhibits correct state-transitions only for a correct key, which is a designer's secret. The proposed easily testable key-controlled FSM synthesis scheme can thwart reverse engineering attacks, thus offers IP protection.
Ermakov, Anton D., Prokopenko, Svetlana A., Yevtushenko, Nina V..  2018.  Security Checking Experiments with Mobile Services. 2018 19th International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices (EDM). :139—141.
In this paper, we continue to investigate the problem of software security. The problem is to check if software under test has some vulnerabilities such as exceeding of admissible values of input/output parameters or internal variables or can reach states where the software (service) behavior is not defined. We illustrate by experiments that the well-known verifier Java Path Finder (JPF) can be utilized for this purpose. We apply JPF-mobile to Android applications and results of security checking experiments are presented.
André, Étienne, Lime, Didier, Ramparison, Mathias, Stoelinga, Mariëlle.  2019.  Parametric Analyses of Attack-Fault Trees. 2019 19th International Conference on Application of Concurrency to System Design (ACSD). :33—42.

Risk assessment of cyber-physical systems, such as power plants, connected devices and IT-infrastructures has always been challenging: safety (i.e., absence of unintentional failures) and security (i. e., no disruptions due to attackers) are conditions that must be guaranteed. One of the traditional tools used to help considering these problems is attack trees, a tree-based formalism inspired by fault trees, a well-known formalism used in safety engineering. In this paper we define and implement the translation of attack-fault trees (AFTs) to a new extension of timed automata, called parametric weighted timed automata. This allows us to parametrize constants such as time and discrete costs in an AFT and then, using the model-checker IMITATOR, to compute the set of parameter values such that a successful attack is possible. Using the different sets of parameter values computed, different attack and fault scenarios can be deduced depending on the budget, time or computation power of the attacker, providing helpful data to select the most efficient counter-measure.

Lago, Loris Dal, Ferrante, Orlando, Passerone, Roberto, Ferrari, Alberto.  2018.  Dependability Assessment of SOA-Based CPS With Contracts and Model-Based Fault Injection. IEEE Transactions on Industrial Informatics. 14:360—369.

Engineering complex distributed systems is challenging. Recent solutions for the development of cyber-physical systems (CPS) in industry tend to rely on architectural designs based on service orientation, where the constituent components are deployed according to their service behavior and are to be understood as loosely coupled and mostly independent. In this paper, we develop a workflow that combines contract-based and CPS model-based specifications with service orientation, and analyze the resulting model using fault injection to assess the dependability of the systems. Compositionality principles based on the contract specification help us to make the analysis practical. The presented techniques are evaluated on two case studies.

Amoroso, E., Merritt, M..  1994.  Composing system integrity using I/O automata. Tenth Annual Computer Security Applications Conference. :34—43.
The I/O automata model of Lynch and Turtle (1987) is summarized and used to formalize several types of system integrity based on the control of transitions to invalid starts. Type-A integrity is exhibited by systems with no invalid initial states and that disallow transitions from valid reachable to invalid states. Type-B integrity is exhibited by systems that disallow externally-controlled transitions from valid reachable to invalid states, Type-C integrity is exhibited by systems that allow locally-controlled or externally-controlled transitions from reachable to invalid states. Strict-B integrity is exhibited by systems that are Type-B but not Type-A. Strict-C integrity is exhibited by systems that are Type-C but not Type-B. Basic results on the closure properties that hold under composition of systems exhibiting these types of integrity are presented in I/O automata-theoretic terms. Specifically, Type-A, Type-B, and Type-C integrity are shown to be composable, whereas Strict-B and Strict-C integrity are shown to not be generally composable. The integrity definitions and compositional results are illustrated using the familiar vending machine example specified as an I/O automaton and composed with a customer environment. The implications of the integrity definitions and compositional results on practical system design are discussed and a research plan for future work is outlined.
Ceška, Milan, Havlena, Vojtech, Holík, Lukáš, Korenek, Jan, Lengál, Ondrej, Matoušek, Denis, Matoušek, Jirí, Semric, Jakub, Vojnar, Tomáš.  2019.  Deep Packet Inspection in FPGAs via Approximate Nondeterministic Automata. 2019 IEEE 27th Annual International Symposium on Field-Programmable Custom Computing Machines (FCCM). :109—117.

Deep packet inspection via regular expression (RE) matching is a crucial task of network intrusion detection systems (IDSes), which secure Internet connection against attacks and suspicious network traffic. Monitoring high-speed computer networks (100 Gbps and faster) in a single-box solution demands that the RE matching, traditionally based on finite automata (FAs), is accelerated in hardware. In this paper, we describe a novel FPGA architecture for RE matching that is able to process network traffic beyond 100 Gbps. The key idea is to reduce the required FPGA resources by leveraging approximate nondeterministic FAs (NFAs). The NFAs are compiled into a multi-stage architecture starting with the least precise stage with a high throughput and ending with the most precise stage with a low throughput. To obtain the reduced NFAs, we propose new approximate reduction techniques that take into account the profile of the network traffic. Our experiments showed that using our approach, we were able to perform matching of large sets of REs from SNORT, a popular IDS, on unprecedented network speeds.

Rajeshwaran, Kartik, Anil Kumar, Kakelli.  2019.  Cellular Automata Based Hashing Algorithm (CABHA) for Strong Cryptographic Hash Function. 2019 IEEE International Conference on Electrical, Computer and Communication Technologies (ICECCT). :1–6.
Cryptographic hash functions play a crucial role in information security. Cryptographic hash functions are used in various cryptographic applications to verify the message authenticity and integrity. In this paper we propose a Cellular Automata Based Hashing Algorithm (CABHA) for generating strong cryptographic hash function. The proposed CABHA algorithm uses the cellular automata rules and a custom transformation function to create a strong hash from an input message and a key.
Fu, Yulong, Li, Guoquan, Mohammed, Atiquzzaman, Yan, Zheng, Cao, Jin, Li, Hui.  2019.  A Study and Enhancement to the Security of MANET AODV Protocol Against Black Hole Attacks. 2019 IEEE SmartWorld, Ubiquitous Intelligence Computing, Advanced Trusted Computing, Scalable Computing Communications, Cloud Big Data Computing, Internet of People and Smart City Innovation (SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI). :1431–1436.
Mobile AdHoc Networks (MANET) can be fast implemented, and it is very popular in many specific network requirements, such as UAV (Unmanned Aerial Unit), Disaster Recovery and IoT (Internet of Things) etc. However, MANET is also vulnerable. AODV (Ad hoc On-Demand Distance Vector Routing) protocol is one type of MANET routing protocol and many attacks can be implemented to break the connections on AODV based AdHoc networks. In this article, aim of protecting the MANET security, we modeled the AODV protocol with one type of Automata and analyzed the security vulnerabilities of it; then based on the analyzing results, we proposed an enhancement to AODV protocol to against the Black Hole Attacks. We also implemented the proposed enhancement in NS3 simulator and verified the correctness, usability and efficiency.
Ayache, Meryeme, Khoumsi, Ahmed, Erradi, Mohammed.  2019.  Managing Security Policies within Cloud Environments Using Aspect-Oriented State Machines. 2019 International Conference on Advanced Communication Technologies and Networking (CommNet). :1—10.

Cloud Computing is the most suitable environment for the collaboration of multiple organizations via its multi-tenancy architecture. However, due to the distributed management of policies within these collaborations, they may contain several anomalies, such as conflicts and redundancies, which may lead to both safety and availability problems. On the other hand, current cloud computing solutions do not offer verification tools to manage access control policies. In this paper, we propose a cloud policy verification service (CPVS), that facilitates to users the management of there own security policies within Openstack cloud environment. Specifically, the proposed cloud service offers a policy verification approach to dynamically choose the adequate policy using Aspect-Oriented Finite State Machines (AO-FSM), where pointcuts and advices are used to adopt Domain-Specific Language (DSL) state machine artifacts. The pointcuts define states' patterns representing anomalies (e.g., conflicts) that may occur in a security policy, while the advices define the actions applied at the selected pointcuts to remove the anomalies. In order to demonstrate the efficiency of our approach, we provide time and space complexities. The approach was implemented as middleware service within Openstack cloud environment. The implementation results show that the middleware can detect and resolve different policy anomalies in an efficient manner.

Noori-Hosseini, Mona, Lennartson, Bengt.  2019.  Incremental Abstraction for Diagnosability Verification of Modular Systems. 2019 24th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA). :393–399.
In a diagnosability verifier with polynomial complexity, a non-diagnosable system generates uncertain loops. Such forbidden loops are in this paper transformed to forbidden states by simple detector automata. The forbidden state problem is trivially transformed to a nonblocking problem by considering all states except the forbidden ones as marked states. This transformation is combined with one of the most efficient abstractions for modular systems called conflict equivalence, where nonblocking properties are preserved. In the resulting abstraction, local events are hidden and more local events are achieved when subsystems are synchronized. This incremental abstraction is applied to a scalable production system, including parallel lines where buffers and machines in each line include some typical failures and feedback flows. For this modular system, the proposed diagnosability algorithm shows great results, where diagnosability of systems including millions of states is analyzed in less than a second.
Mercaldo, Francesco, Martinelli, Fabio, Santone, Antonella.  2019.  Real-Time SCADA Attack Detection by Means of Formal Methods. 2019 IEEE 28th International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE). :231–236.
SCADA control systems use programmable logic controller to interface with critical machines. SCADA systems are used in critical infrastructures, for instance, to control smart grid, oil pipelines, water distribution and chemical manufacturing plants: an attacker taking control of a SCADA system could cause various damages, both to the infrastructure but also to people (for instance, adding chemical substances into a water distribution systems). In this paper we propose a method to detect attacks targeting SCADA systems. We exploit model checking, in detail we model logs from SCADA systems into a network of timed automata and, through timed temporal logic, we characterize the behaviour of a SCADA system under attack. Experiments performed on a SCADA water distribution system confirmed the effectiveness of the proposed method.
Danger, Jean-Luc, Fribourg, Laurent, Kühne, Ulrich, Naceur, Maha.  2019.  LAOCOÖN: A Run-Time Monitoring and Verification Approach for Hardware Trojan Detection. 2019 22nd Euromicro Conference on Digital System Design (DSD). :269–276.

Hardware Trojan Horses and active fault attacks are a threat to the safety and security of electronic systems. By such manipulations, an attacker can extract sensitive information or disturb the functionality of a device. Therefore, several protections against malicious inclusions have been devised in recent years. A prominent technique to detect abnormal behavior in the field is run-time verification. It relies on dedicated monitoring circuits and on verification rules generated from a set of temporal properties. An important question when dealing with such protections is the effectiveness of the protection against unknown attacks. In this paper, we present a methodology based on automatic generation of monitoring and formal verification techniques that can be used to validate and analyze the quality of a set of temporal properties when used as protection against generic attackers of variable strengths.

Yang, J., Jeong, J. P..  2018.  An Automata-based Security Policy Translation for Network Security Functions. 2018 International Conference on Information and Communication Technology Convergence (ICTC). :268–272.

This paper proposes the design of a security policy translator in Interface to Network Security Functions (I2NSF) framework. Also, this paper shows the benefits of designing security policy translations. I2NSF is an architecture for providing various Network Security Functions (NSFs) to users. I2NSF user should be able to use NSF even if user has no overall knowledge of NSFs. Generally, policies which are generated by I2NSF user contain abstract data because users do not consider the attributes of NSFs when creating policies. Therefore, the I2NSF framework requires a translator that automatically finds the NSFs which is required for policy when Security Controller receives a security policy from the user and translates it for selected NSFs. We satisfied the above requirements by modularizing the translator through Automata theory.

Goncharov, N. I., Goncharov, I. V., Parinov, P. A., Dushkin, A. V., Maximova, M. M..  2019.  Modeling of Information Processes for Modern Information System Security Assessment. 2019 IEEE Conference of Russian Young Researchers in Electrical and Electronic Engineering (EIConRus). :1758-1763.

A new approach of a formalism of hybrid automatons has been proposed for the analysis of conflict processes between the information system and the information's security malefactor. An example of probability-based assessment on malefactor's victory has been given and the possibility to abstract from a specific type of probability density function for the residence time of parties to the conflict in their possible states. A model of the distribution of destructive informational influences in the information system to connect the process of spread of destructive information processes and the process of changing subjects' states of the information system has been proposed. An example of the destructive information processes spread analysis has been given.

Frolov, A. B., Vinnikov, A. M..  2018.  Modeling Cryptographic Protocols Using the Algebraic Processor. 2018 IV International Conference on Information Technologies in Engineering Education (Inforino). :1–5.

We present the IT solution for remote modeling of cryptographic protocols and other cryptographic primitives and a number of education-oriented capabilities based on them. These capabilities are provided at the Department of Mathematical Modeling using the MPEI algebraic processor, and allow remote participants to create automata models of cryptographic protocols, use and manage them in the modeling process. Particular attention is paid to the IT solution for modeling of the private communication and key distribution using the processor combined with the Kerberos protocol. This allows simulation and studying of key distribution protocols functionality on remote computers via the Internet. The importance of studying cryptographic primitives for future IT specialists is emphasized.

Bobda, C., Whitaker, T. J. L., Kamhoua, C., Kwiat, K., Njilla, L..  2017.  Synthesis of Hardware Sandboxes for Trojan Mitigation in Systems on Chip. 2017 IEEE International Symposium on Hardware Oriented Security and Trust (HOST). :172–172.

In this work, we propose a design flow for automatic generation of hardware sandboxes purposed for IP security in trusted system-on-chips (SoCs). Our tool CAPSL, the Component Authentication Process for Sandboxed Layouts, is capable of detecting trojan activation and nullifying possible damage to a system at run-time, avoiding complex pre-fabrication and pre-deployment testing for trojans. Our approach captures the behavioral properties of non-trusted IPs, typically from a third-party or components off the shelf (COTS), with the formalism of interface automata and the Property Specification Language's sequential extended regular expressions (SERE). Using the concept of hardware sandboxing, we translate the property specifications to checker automata and partition an untrusted sector of the system, with included virtualized resources and controllers, to isolate sandbox-system interactions upon deviation from the behavioral checkers. Our design flow is verified with benchmarks from, which show 100% trojan detection with reduced checker overhead compared to other run-time verification techniques.

Sugumar, G., Mathur, A..  2017.  Testing the Effectiveness of Attack Detection Mechanisms in Industrial Control Systems. 2017 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C). :138–145.

Industrial Control Systems (ICS) are found in critical infrastructure such as for power generation and water treatment. When security requirements are incorporated into an ICS, one needs to test the additional code and devices added do improve the prevention and detection of cyber attacks. Conducting such tests in legacy systems is a challenge due to the high availability requirement. An approach using Timed Automata (TA) is proposed to overcome this challenge. This approach enables assessment of the effectiveness of an attack detection method based on process invariants. The approach has been demonstrated in a case study on one stage of a 6- stage operational water treatment plant. The model constructed captured the interactions among components in the selected stage. In addition, a set of attacks, attack detection mechanisms, and security specifications were also modeled using TA. These TA models were conjoined into a network and implemented in UPPAAL. The models so implemented were found effective in detecting the attacks considered. The study suggests the use of TA as an effective tool to model an ICS and study its attack detection mechanisms as a complement to doing so in a real plant-operational or under design.

Sun, C., Xi, N., Ma, J..  2017.  Enforcing Generalized Refinement-Based Noninterference for Secure Interface Composition. 2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC). 1:586–595.

Information flow security has been considered as a critical requirement on complicated component-based software. The recent efforts on the compositional information flow analyses were limited on the expressiveness of security lattice and the efficiency of compositional enforcement. Extending these approaches to support more general security lattices is usually nontrivial because the compositionality of information flow security properties should be properly treated. In this work, we present a new extension of interface automaton. On this interface structure, we propose two refinement-based security properties, adaptable to any finite security lattice. For each property, we present and prove the security condition that ensures the property to be preserved under composition. Furthermore, we implement the refinement algorithms and the security condition decision procedure. We demonstrate the usability and efficiency of our approach with in-depth case studies. The evaluation results show that our compositional enforcement can effectively reduce the verification cost compared with global verification on composite system.

Madhusudhanan, S., Mallissery, S..  2017.  Provable security analysis of complex or smart computer systems in the smart grid. 2017 IEEE International Conference on Smart Grid and Smart Cities (ICSGSC). :210–214.

Security is an important requirement of every reactive system of the smart gird. The devices connected to the smart system in smart grid are exhaustively used to provide digital information to outside world. The security of such a system is an essential requirement. The most important component of such smart systems is Operating System (OS). This paper mainly focuses on the security of OS by incorporating Access Control Mechanism (ACM) which will improve the efficiency of the smart system. The formal methods use applied mathematics for modelling and analysing of smart systems. In the proposed work Formal Security Analysis (FSA) is used with model checking and hence it helped to prove the security of smart systems. When an Operating System (OS) takes into consideration, it never comes to a halt state. In the proposed work a Transition System (TS) is designed and the desired rules of security are provided by using Linear Temporal Logics (LTL). Unlike other propositional and predicate logic, LTL can model reactive systems with a prediction for the future state of the systems. In the proposed work, Simple Promela Interpreter (SPIN) is used as a model checker that takes LTL and TS of the system as input. Hence it is possible to derive the Büchi automaton from LTL logics and that provides traces of both successful and erroneous computations. Comparison of Büchi automaton with the transition behaviour of the OS will provide the details of security violation in the system. Validation of automaton operations on infinite computational sequences verify that whether systems are provably secure or not. Hence the proposed formal security analysis will provably ensures the security of smart systems in the area of smart grid applications.