Qualification: 
Ph.D
jayarajp@am.amrita.edu

Dr. Jayaraj Poroor, currently serves as the Chairperson at the Department of Computer Science (CSA/CSE), Amrita School of Engineeirng, Amritapuri campus. 

Publications

Publication Type: Journal Article

Year of Publication Publication Type Title

2018

Journal Article

T. M. G, Somasundaram, K., and Jayaraj Poroor, “ Analysis of Numerical Accuracy in Floating Point Programs Using Abstract Interpretation”, AFMSS, Springer LNCS (in print), 2018.

2013

Journal Article

Jayaraj Poroor and Bharat Jayaraman, “Modeling mobile stateful channels in πZ”, Science of Computer Programming, vol. 78, pp. 1470 - 1489, 2013.[Abstract]


We investigate a principled extension of the π-calculus for formal modeling of mobile communicating systems with stateful channels. In our proposed extension, called πZ, a channel is associated with a stateful abstract type in the Z specification language. We develop both reduction as well as labeled transition semantics for πZ. We show that the important properties of the π-calculus are preserved in πZ: (1) τ-transitions match reductions; and (2) bisimilarity induced by the labeled transitions is closed under parallel composition, name restriction, and a restricted recursion. The paper illustrates the use of stateful channels by modeling the ‘hidden node problem’ in a wireless network.

More »»

2012

Journal Article

Jayaraj Poroor and Bharat Jayaraman, “C2L:A Formal Policy Language for Secure Cloud Configurations”, Procedia Computer Science, vol. 10, pp. 499 - 506, 2012.[Abstract]


We present a formal policy language (C2L) for stating permissible cloud configurations. Syntactically, C2L is based upon a spatio-temporal modal logic and provides a concise and clear statement of policy constraints for colocation, hosting, migration, security, andavailability.We illustrate the language witha numberof policyspecificationexamples and also present an algorithm forverifying whethera cloud configuration along with its history satisfiesaC2Lpolicy specification.We provide complexity analysisof the algorithm, and conclude thatC2Lisa useful and viable formalism for specifying and verifying cloud configuration policies

More »»

2011

Journal Article

Jayaraj Poroor and Jayaraman, Bb, “Verifying security properties of internet protocol stacks: The split verification approach”, Journal of Systems Architecture, vol. 57, pp. 269-281, 2011.[Abstract]


We propose a novel method to construct user-space internet protocol stacks whose security properties can be formally explored and verified. The proposed method allows construction of protocol stacks using a C++ subset. We define a formal state-transformer representation of protocol stacks in which the protocol stack is specified in terms of three primary operations, which are constructed from sub-operations, in a compositional manner. We also define a Kripke model that captures the sequencing and attributes of stack operations. We propose a novel approach, called split verification, which combines theorem-proving and model-checking to establish properties for a protocol stack specification. In split verification, properties to be established for the stack are expressed as a combination of properties for primitive operations to be established via theorem-proving as well as temporal properties on operation sequencing, called promotion conditions, to be established via model-checking on the stack operations model. We use abstract Z specifications to represent operation properties and computational tree logic (CTL) formulae to represent promotion conditions. Operation properties are established by checking whether the operation(s) under consideration are correct refinements of the abstract Z specification(s). Our conclusion is that split verification: (a) avoids scalability issues caused by state-space explosion in model-checking and long unwieldy proofs in theorem-proving, and, (b) lowers cost of proof maintenance for localized changes in the stack.

More »»

2009

Journal Article

Jayaraj Poroor and Jayaraman, B., “DoS Attacks on Real-Time Media through Indirect Contention-in-Hosts”, IEEE Internet Computing, vol. 13, pp. 22-30, 2009.[Abstract]


Quality of service (QoS) is critical for delivering real-time media services (RTMSs). The authors identify a new class of denial-of-service attacks against RTMSs - indirect contention-in-hosts (ICiH). Here, attackers attempt to indirectly degrade RTMS QoS by directing packets at other concurrent services, thereby inducing resource contention between RTMS packets and attack packets in the protocol stack. To analyze such attacks, the authors' operation-trace analysis method formalizes the notion of contention among concurrent services and develops several metrics to quantify ICiH's effects.

More »»

Publication Type: Conference Paper

Year of Publication Publication Type Title

2018

Conference Paper

Jayaraj Poroor, “Verticalthings - a Language-based Microkernel for Constrained IoT Devices: Work-in-progress”, in Proceedings of the International Conference on Embedded Software, Piscataway, NJ, USA, 2018.[Abstract]


A programming language that provides the functions of a secure microkernel is proposed for embedded and IoT applications. Towards this purpose, a type system based on the capability model is proposed, in which resource classes are abstracted as capability classes. Our language enables static analysis of key properties including safety, security, power, and timing considerations.

More »»

2017

Conference Paper

H. Narayanan, Radhakrishnan, V., Shiju Sathyadevan, and Jayaraj Poroor, “Architectural Design for a Secure Linux Operating System”, in 2017 International Conference on Wireless Communications, Signal Processing and Networking (WiSPNET), 2017.[Abstract]


Operating system security is a hot research area for the past several decades. Various security mechanisms have been introduced till now to secure the operating system. In this paper we are focusing on securing Linux operating system. Even though Linux is open source and large numbers of people are involved in developing kernel patches for security holes, there are still many malwares to exploit the existing vulnerabilities. Using our architecture we are trying to minimize the damage done by the malwares if not blocking them altogether. Our architecture is designed to ensure the principle of least privilege. Principle of least privilege guarantees that a process will get the privileges just enough to perform its task. This ensures that even if the process is compromised it can do the least damage to the system as it is running in a sandbox. Major chunk of our system is running in the user level to make it portable across the distributions. Our system uses a specially structured security ticket to provide fine grained authorization to user processes which is not currently possible in the traditional linux architecture. The security ticket is designed in such a way that it can be inherited by a child process, can be shared and is unforgeable. The core module in the system is called Secd (Secure Daemon) which authorizes all the requests and also manages the security tickets.

More »»

2017

Conference Paper

Jayaraj Poroor, “The Energy Computer: A Novel Internet-of-Things (IoT) Device for Improved Energy Productivity”, in 2017 International Conference on Technological Advancements in Power and Energy ( TAP Energy), 2017.[Abstract]


The Energy Computer, an Internet-of-Things (IoT) device for monitoring the behaviour of electrical machinery by analyzing the electrical parameters in real-time is presented. In order to achieve this while maintaining low energy footprint, we designed and built a Virtual Machine Operating System (VMOS) with extremely low memory footprint, consequently low energy footprint. Applications for aggregating and analyzing data in real-time can be downloaded to the device and executed on the top of VMOS. One or more such applications, executing on the device, can perform real-time data aggregation and analysis by implementing algorithms and logic specific to an industry domain or specific to a class of industrial machinery. The device is built using a dual microcontroller architecture, the primary microcontroller featuring Ferroelectric RAM (FRAM) technology, executes our VMOS as well as its apps that perform real-time data analysis. The secondary microcontroller provides a full WiFi-based network stack for data access even when Internet connectivity is absent. The entire hardware and software for the device has been designed and built from ground up. The device has been thoroughly field tested in small and medium-sized industrial units in Mumbai, Ahmedabad, and Bangalore.

More »»

2015

Conference Paper

Shiju Sathyadevan, Krishnasree Achuthan, and Jayaraj Poroor, “Architectural Recommendations in Building a Network Based Secure, Scalable and Interoperable Internet of Things Middleware”, in 3rd International Conference on Frontiers of Intelligent Computing: Theory and Applications (FICTA) 2014, Cham, 2015, vol. 1, pp. 429–439.[Abstract]


With every device capable of emitting data, the need to amass and process them in real time or near real time, along with ever growing user requirement of, information-on-demand, have paved the way for the sudden surge in the development of the theme Internet of Things (IoT). Even though this whole new technology looks fascinating in theory, its practical implementation and ongoing sustenance is something that will need a lot of thought, effort and careful planning. Several cloud based and network based cloud platforms/middleware solutions are available but a lot of them are either extremely complex to set up, or needs standardized solutions to be applied across all participating devices or would leave behind vivid security loopholes that can’t be curbed with ease considering the overall capability of the devices involved. Based on a previous research effort conducted by our team, detailed scrutiny of prominent existing IoT platforms/middleware solutions were performed. This effort has resulted in defining the core problem matrix which if addressed adequately could result in the development of a well balanced IoT middleware solution. This paper uses the problem matrix so identified as the roadmap in defining a Secure, Scalable, Interoperable Internet of Things Middleware.

More »»

2012

Conference Paper

Jayaraj Poroor and Jayaraman, Bb, “Formal analysis of event-driven cyber physical systems”, in ACM International Conference Proceeding Series, Kerala, 2012, pp. 1-8.[Abstract]


We propose a programming language (E#) that facilitates formal verification of security properties of event-driven cy- berphysical systems. We describe the syntax of E# with the help of several illustrative examples. Since the environment plays a crucial role in cyberphysical systems, E# facilitates modeling of the environment processes abstractly using the novel 'causes' clauses. We show that event causality graphs (ECGs) may be constructed from causes clauses and handle specifications. We present how ECGs can be used to detect compute-bound event loops which are undesirable in event- driven systems and also to analyze response-style event live- ness specifications. We show how safety properties can be inductively established by employing either theorem-proving or model checking. This technique facilitates compositional verification, allowing us to establish properties of each component separately. The technique also avoids state explosion that arises due to interleaving of the atomic blocks of concurrent event handlers. An interesting feature of our safety analysis is our use of model checking for safety properties in an inductive setting. We conclude that E# is a viable language for programming safety-critical event-driven cyber- physical systems. Copyright 2012 ACM.

More »»

2011

Conference Paper

Jayaraj Poroor and Jayaraman, Bb, “Formal specification and verification of vehicular handoff using π-calculus”, in ACWR 2011 - Proceedings of the International Conference on Wireless Technologies for Humanitarian Relief, Amritapuri, 2011, pp. 165-168.[Abstract]


Vehicular networking is an important emerging area having immense applications, ranging from road-safety to emergency communications in disaster situations. As more applications begin to take advantage of vehicular networks, correctness of the underlying protocols must be subjected to rigorous analysis. The π-calculus is a formal language for specifying mobile systems and has been applied in wide range of settings, from specifying security protocols to modeling biomolecular systems. In this paper, we use π-calculus to construct a formal specification of a cross-layer dual-radio handoff algorithm for vehicular networks. The main challenge in this work was to use the minimal set of highly expressive and powerful constructs of π-calculus to model protocol agents at the right level of abstraction. To give two instances of our approach: (a) the two radios involved in handoff are modelled as concurrent sub-processes of the mobile node process; (b) route to the gateway is modelled as a channel that the access point supplies to both the gateway and the mobile node, both of which are modelled as concurrent processes. We formulate representative properties in a branching-time temporal logic and verify our protocol specification against these properties. Our study shows that π-calculus is a suitable formalism for modeling and verifying vehicular protocols.

More »»