Qualification: 
Ph.D
Email: 
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

2013

Journal Article

B. Jayaraman and Jayaraj Poroor, “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

B. Jayaraman and Jayaraj Poroor, “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

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 »»
207
PROGRAMS
OFFERED
5
AMRITA
CAMPUSES
15
CONSTITUENT
SCHOOLS
A
GRADE BY
NAAC, MHRD
8th
RANK(INDIA):
NIRF 2018
150+
INTERNATIONAL
PARTNERS
  • Amrita on Social Media

  • Contact us

    Amrita Vishwa Vidyapeetham
    Amritanagar, Coimbatore - 641 112
    Tamilnadu, India
    • Fax: +91-422-2686274
    • Coimbatore : +91 (422) 2685000
    • Amritapuri   : +91 (476) 280 1280
    • Bengaluru    : +91 (080) 251 83700
    • Kochi              : +91 (484) 280 1234
    • Mysuru          : +91 (821) 234 3479
    • Contact Details »