Embedded systems for low latency safety-critical applications such as autonomous vehicles, space flight systems, large-scale chemical, energy and nuclear systems require formal guarantees on the input received at runtime prior to data processing. A common unintended behavior arising in communication over a network is that packets may arrive out-of-order and typically application layer protocols require underlying transport layer packets to arrive in order to ensure Quality of Service (QoS). In this context, if a processor is available to buffer and check events received over the network for safe execution, it is possible to deploy a Runtime Enforcement (RE) framework to guarantee that the protected system receives input that satisfies a set of formally defined properties. However, most current RE frameworks do not consider the order of events while processing their configured policies which makes them less viable to low latency safety-critical applications. This work proposes a new formal RE paradigm which handles event reordering for any regular property specified as an automaton. We formally define the RE framework, develop an online enforcement algorithm, and prove its correctness. We illustrate that our enforcer implementation is latency-sensitive by reasoning about the influence of out-of-order events in all possible future paths. We analyze the limits of memory utilization for enforcement theoretically for a few classes of regular properties along with extensive performance evaluation across a wide range of input lengths and properties. This includes testing the limits of the latency-sensitive implementation and its practical effectiveness against a safety-critical case-study on smart switches.
@inproceedings{ictac_reorder,author={{Pradhan}, A. and {Akil}, C. G. Mitun and {Pinisetty}, S.},title={Runtime Enforcement with Event Reordering},booktitle={International Colloquium on Theoretical Aspects of Computing (ICTAC),},year={2024}}
Runtime Enforcement (RE) is a technique aimed at monitoring the executions of a system at runtime and ensure its compliance against a set of formal requirements (properties). RE employs an enforcer (a safety wrapper for the system) which modifies the (untrustworthy) output by performing actions such as delaying (by storing/buffering) and suppressing events, when needed. In this paper, to handle practical applications with memory constraints, we propose a new RE paradigm where the memory of the enforcer is bounded/finite. Besides the property to be enforced, the user specifies a bound on the enforcer memory. Bounding the memory poses various challenges such as how to handle the situation when the memory is full, how to optimally discard events from the buffer to accommodate new events and let the enforcer continue operating. We define the bounded-memory RE problem and develop a framework for any regular property. All of our results are formalized and proved. We also analyze probabilistically how much memory is required on an average case for a given regular property, such that the output of the bounded enforcer is equal to that of the unbounded enforcer up to a fixed probability. The proposed framework is implemented and a case study is worked out to show the practicability and usefulness of the bounded enforcer in the real-world and to show the usage of the aforementioned probabilistic analysis on them. The performance is evaluated via some examples from application scenarios and it indicates linear changes in the execution time of the enforcers in response to increases in trace length, property complexity, and buffer sizes.
@article{bmre_fmsd,author={{Shankar}, S. and {Pradhan}, A. and {Pinisetty}, S. and {Rollet}, A. and {Falcone}, Y.},title={Bounded-memory runtime enforcement with probabilistic and performance analysis},journal={Formal Methods in System Design,},year={2024},volume={62},pages={141-180},doi={10.1007/s10703-024-00446-1},url={https://link.springer.com/article/10.1007/s10703-024-00446-1},}
Spiking Neural Networks (SNNs) have found increasing utility in designing safety-critical Cyber-Physical Systems (CPSs) such as implantable medical devices, autonomous vehicles, and space robotics due to their capability to operate on information represented in temporal coding and exhibit various behavioural modalities. Thus, there has been recent interest in formally verifying their timing behaviours and providing soundness guarantees of their diverse characteristics. However, beyond the simplistic Leaky Integrate and Fire (LIF) model, which only mimics 3 spiking behaviours, there is a lack of unifying methodology in literature to verify complex dynamics of biological neurons exhibiting 20 spiking behaviours as demonstrated by the pioneering work of Izhikevich. There is also a complete lack of formulation for the verification of SNN-based systems. This paper bridges these gaps by proposing a model-based approach for designing SNN-based controllers in CPS. We propose sound structural transformations translating any spiking neuron into networks of Timed Automata (TA), model the complex Izhikevich neural model and formally verify all 20 timing behaviours it exhibits for the first time. We then present two case studies that were modelled as SNNs using our approach: the PID controller, and the Car-Following controller, and subsequently attempt static model checking and statistical verification of their generated TA models for safety guarantees.
@article{izhi_tc_cs,author={{Pradhan}, A. and {King}, J. and {Pinisetty}, S. and {Roop}, P.},title={Model based verification of spiking neural networks in cyber physical systems},journal={IEEE Transactions on Computers,},year={2023},volume={},doi={10.1109/TC.2023.3251841}}
Runtime enforcement is a methodology used to enforce that the output of a running system satisfies a desired property. Given a property, an enforcement monitor modifies an (untrusted) sequence of events into a sequence that complies to that property. In practice, we may have not one, but many properties to enforce. Moreover, new properties may arise as new capabilities are added to the system. It is thus important to construct not a single, i.e., monolithic monitor, but rather several monitors, one for each property. The question is to what extent such monitors can be composed, and how. In this paper, we study two enforcement monitor composition schemes, serial and parallel composition. We show that, runtime enforcement is compositional for general regular properties with respect to one of the parallel composition schemes defined. We also show that runtime enforcement is not compositional with respect to serial composition for general regular properties, but it is for certain subclasses of regular properties. The proposed compositional runtime enforcement framework is formalized and implemented. Our experimental results demonstrate the pros and cons of using the compositional approach versus the monolithic with respect to performance.
@article{pcre_fmsd,author={{Pinisetty}, S. and {Pradhan}, A. and {Roop}, P. and {Tripakis}, S.},title={Compositional runtime enforcement revisited},journal={Formal Methods in System Design,},year={2022},volume={59},pages={205-252},doi={10.1007/s10703-022-00401-y},url={https://link.springer.com/article/10.1007/s10703-022-00401-y},}
Attribute-based encryption (ABE) has evolved as an efficient and secure method for storage of data with fine-grained access control in cloud platforms. In recent years, increasing diversification in the design of ABE schemes has led to significant research in the assimilation of properties like traceability, revocation, and outsourcing decryption. However, most of the recent ABE schemes incorporate few of these properties and hence lack in robustness to adapt with varying demands of cloud systems. In modern ABE designs, the notions of forward and backward secrecy have been introduced to accommodate the delegation of a large number of heterogeneous users in the system. In general, these features are realized under the concept of user revocation. On the other hand, to control malicious users in the system, it is necessary to implement traceability in integration with user revocation. Finally, for resource-constrained users, outsourcing decryption to proxy servers is a viable option. Thus, we propose PMTER-ABE, a practical decentralized multi-authority traceable and efficiently revocable attribute-based cryptosystem with outsourcing decryption advantage. The key features of our cryptosystem are (i) incorporating large attribute universe with highly expressive policies, (ii) integrating forward and backward secrecy under user revocation, (iii) implementing white-box traceability to detect malicious users, and (iv) outsourcing decryption to reduce the computational overhead of decryption on users. We present the formal proofs for correctness, security, and traceability of PMTER-ABE along with performance analysis. The efficiency and usability of PMTER-ABE is shown with practical implementation and experimental results.
@article{cc_pmterabe,author={{Sethi}, K. and {Pradhan}, A. and {Bera}, P.},title={PMTER-ABE: a practical multi-authority CP-ABE with traceability, revocation and outsourcing decryption for secure access control in cloud systems},journal={Cluster Computing,},year={2021},volume={24},issn={1573-7543},doi={10.1007/s10586-020-03202-2},url={https://link.springer.com/article/10.1007/s10586-020-03202-2}}
Let \(G\) be a simple graph. By an independent set in \(G\), we mean a set of pairwise non-adjacent vertices in \(G\). The independence polynomial of \(G\) is defined as \(I_G(z)=i_0 + i_1 z + i_2 z^2+⋯+i_αz^α\), where \(i_m=i_m(G)\) is the number of independent sets in \(G\) with cardinality \(m\) and \(α=α(G)\) denotes the cardinality of a largest independent set in \(G\) (known as the independence number of \(G\)). Let \(G^k\) denote the \(k\)-times lexicographic product of \(G\) with itself. The set of roots of \(I_{G^k}\) is known to converge as \(k\) tends to \(∞\), with respect to the Hausdorff metric, and the limiting set is known as the independence attractor. The independence fractal of a graph is the limiting set of roots of the reduced independence polynomial \(I_{G^k}-1\) of \(G^k\) as \(k\) tends to \(∞\). In this article, we consider the independence fractals of graphs with independence number \(3\). We attempt to find all such graphs whose independence fractal is a line segment. It is shown that the independence fractal and the independence attractor coincide when the earlier is a line segment. The line segment turns out to be an interval \([-\frac4k, 0]\) for \(k ∈{1, 2, 3, 4}\). It is found that each of these graphs have \(9\) vertices and there are exactly \(13\) such disconnected graphs. We show that there does not exist any connected graph for \(k = 4\). For \(k = 1\), there are \(17\) such connected graphs and for \(k = 2, 3\) the number is quite large.
@article{ind_fractal,author={{Barik}, S. and {Nayak}, T. and {Pradhan}, A.},title={Graphs Whose Independence Fractals are Line Segments},journal={Bulletin of the Malaysian Mathematical Sciences Society,},year={2021},volume={44},pages={55-78},doi={10.1007/s40840-020-00936-5},url={https://link.springer.com/article/10.1007/s40840-020-00936-5}}
Smart grid employs intelligent transmission and distribution networks for effective and reliable delivery of electricity. It uses fine-grained electrical measurements to attain optimized reliability and stability by sharing these measurements among different entities of energy management systems of the grid. There are many stakeholders like users, phasor measurement units (PMU), and other entities, with changing requirements involved in the sharing of the data. Therefore, data security plays a vital role in the correct functioning of a power grid network. In this paper, we propose an attribute-based encryption (ABE) for secure data sharing in Smart Grid architectures as ABE enables efficient and secure access control. Also, the access policy is obfuscated to preserve privacy. We use Linear Secret Sharing (LSS) Scheme for supporting any monotone access structures, thereby enhancing the expressiveness of access policies. Finally, we also analyze the security, access policy privacy and collusion resistance properties along with efficiency analysis of our cryptosystem.
@inproceedings{COMNSNETS_ABE,author={{Sethi}, K. and {Pradhan}, A. and {Bera}, P.},booktitle={2020 International Conference on COMmunication Systems NETworkS (COMSNETS),},title={Attribute-Based Data Security with Obfuscated Access Policy for Smart Grid Applications},year={2020},volume={},number={},doi={10.1109/COMSNETS48256.2020.9027398},pages={503-506},}
Multi-authority ciphertext policy attribute-based encryption (CP-ABE) is one of the promising approaches where multiple authorities issue and manage various attributes to achieve fine-grained access control on stored data in cloud platforms. However, the practical use of multi-authority CP-ABE (MCP-ABE) requires satisfaction of different features. Firstly, in MCP-ABE, users having the same set of attributes must share the same decryption privileges. This may potentially lead to exposure of decryption keys by some malicious users. Thus, there is a need of designing MCP-ABE with traceability to overcome this problem. Secondly, as the cost of decryption increases with the complexity of access policy, it is preferred to provide the functionality of outsourcing decryption to reduce the computational burden on the user. Finally, the data owners must have flexibility to change the access policy. Hence, policy updation must be an integral part of MCP-ABE scheme. In this paper, we construct a new multi-authority CP-ABE scheme over large attribute universe with decentralization of authorities that supports white-box traceability along with policy updation and outsourcing decryption. Our proposed cryptosystem is built on prime order groups and supports monotonic access structures. These features improve efficiency and expressiveness of our system. We implemented our proposed cryptosystem in Charm cryptographic framework and analyzed its performance with a diverse set of test cases.
@article{jisa_polUpdate,author={{Sethi}, K. and {Pradhan}, A. and {Bera}, P.},title={Practical traceable multi-authority CP-ABE with outsourcing decryption and access policy updation},journal={Journal of Information Security and Applications,},volume={51},pages={102435},year={2020},issn={2214-2126},doi={10.1016/j.jisa.2019.102435},url={http://www.sciencedirect.com/science/article/pii/S2214212619305381}}
In recent years, cyberbullying has grown out of proportion due to the increasing usage of social media platforms along with the benefit of user anonymization over the Internet. Affecting people across all demographics, the effect of cyberbullying has been more pronounced over adolescents and insecure individuals. Victims suffer from societal isolation, depression, degrading self-confidence and suicidal thoughts. Thus, prevention of cyberbullying becomes a necessity and requires timely detection. Recent advances in Deep learning and Natural Language Processing have provided suitable models to predict whether a text sample is an example of cyberbullying. In this context, we explore the adaptivity and efficiency of self-attention models in detecting cyberbullying. Though a few of the recent works in this context have employed models like deep neural networks, SVM, CNN, LSTM and other hybrid models, to the best of our knowledge, this is the first work exploring self-attention models which have achieved state-of-the-art accuracies in Machine Translation tasks since 2017. We experiment with the Wikipedia, Formspring and Twitter cyberbullying datasets and achieve more efficient results over existing cyberbullying detection models. We also propose new research directions within cyberbullying detection over recent forms of media like Internet memes which pose a variety of new and hybrid problems.
@inproceedings{self_attention_cbd,author={{Pradhan}, A. and {Yatam}, V. M. and {Bera}, P.},booktitle={2020 International Conference on Cyber Situational Awareness, Data Analytics and Assessment (CyberSA),},title={Self-Attention for Cyberbullying Detection},year={2020},volume={},number={},doi={10.1109/CyberSA49311.2020.9139711},pages={1-6},video={https://www.youtube.com/watch?v=qdAdhXjR0BQ},}
Smart grid consists of multiple different entities related to various energy management systems which share fine-grained energy measurements among themselves in an optimal and reliable manner. Such delivery is achieved through intelligent transmission and distribution networks composed of various stakeholders like Phasor Measurement Units (PMUs), Master and Remote Terminal Units (MTU and RTU), Storage Centers and users in power utility departments subject to volatile changes in requirements. Hence, secure accessibility of data becomes vital in the context of efficient functioning of the smart grid. In this paper, we propose a practical attribute-based encryption scheme for securing data sharing and data access in Smart Grid architectures with the added advantage of obfuscating the access policy. This is aimed at preserving data privacy in the context of competing smart grid operators. We build our scheme on Linear Secret Sharing (LSS) Schemes for supporting any monotone access structures and thus enhancing the expressiveness of access policies. Lastly, we analyze the security, access policy privacy and collusion resistance properties of our cryptosystem and provide an efficiency comparison as well as experimental analysis using the Charm-Crypto framework to validate the proficiency of our proposed solution.
@inproceedings{smart_grid_full_conf,author={{Pradhan}, A. and {Punith}, R. and {Sethi}, K. and {Bera}, P.},booktitle={2020 International Conference on Cyber Situational Awareness, Data Analytics and Assessment (CyberSA),},title={Smart Grid Data Security using Practical CP-ABE with Obfuscated Policy and Outsourcing Decryption},year={2020},volume={},number={},doi={10.1109/CyberSA49311.2020.9139628},pages={1-8},}
Cellular automata (CA) has attracted the attention of research communities for its applications in the design of symmetric and public-key cryptosystems. The strength of cellular automata lies in its inherent data parallelism, which can help accelerate access control mechanisms, and its information scrambling capabilities, which can enhance the security of the system. Also, the cryptosystems designed using CA do not involve number-theoretic methodologies that incur large computational overhead like traditional cryptosystems. However, existing CA-based cryptosystems encompass a limited set from the set of all possible transition rules indicating the existence of CA cryptosystems which are possibly unbreakable but have not been explored sufficiently. Thus, they have not yet been considered for applications involving fine-grained access control for heterogeneous access to the data. In this paper, we propose a secure distributed multi-authority attribute-based encryption using CA, which has potential applications in cloud systems. Our cryptosystem adopts the concept of multi-authority attribute-based access control where the encryption and attribute distribution use reversible CA, and policy satisfiability is achieved by Turing-complete CA in a distributed environment. We illustrate the practical usability of our proposed cryptosystem, in terms of efficiency and security, by extensive experimental results.
@inproceedings{cans_CA,editor={Mu, Yi and Deng, Robert H. and Huang, Xinyi},title={Distributed Multi-authority Attribute-Based Encryption Using Cellular Automata},booktitle={Cryptology and Network Security (CANS),},year={2019},publisher={Springer International Publishing},address={Cham},pages={434--456},doi={10.1007/978-3-030-31578-8_24},isbn={978-3-030-31578-8},author={{Pradhan}, A. and {Sethi}, K. and {Mohapatra}, S. and {Bera}, P.},}
Today a large volume of data is stored in cloud that requires fine grained accessibility for heterogeneous users. Cipher-text policy attribute based encryption (CP-ABE) has evolved into a promising solution for secure data storage with fine grained access control. In CP-ABE, the ciphertext is associated with an access policy (set of rules) and users can access the data if their attributes satisfies the access policy. However, existing CP-ABE schemes fail to perform in presence of large number of users and hierarchical relationships among them. Moreover, a majority of the CP-ABE schemes require large computational overhead for light weight applications. In this paper, we present a hierarchical attribute based cryptosystem by introducing hierarchical dependency between the users and thereby achieving multi-layer verification for fine grained data access. Moreover, our proposed cryptosystem is seamless to user revocation. The efficiency and security of our proposed cryptosystem have been analyzed and reported. Further we implement the proposed cryptosystem in Charm to demonstrate its practicality.
@inproceedings{CyberScience_HABE,author={{Sethi}, K. and {Pradhan}, A. and {Punith}, R. and {Bera}, P.},booktitle={2019 International Conference on Cyber Security and Protection of Digital Services (Cyber Security),},title={A Scalable Attribute Based Encryption for Secure Data Storage and Access in Cloud},year={2019},volume={},number={},doi={10.1109/CyberSecPODS.2019.8884981},pages={1-8}}