Nadeem Akhtar

Neil Dalal, Nadeem Akhtar, Anubhav Gupta et al.

Wi-Fi (802.11) networks have become an essential part of our daily lives; hence, their security is of utmost importance. However, Wi-Fi Protected Access 3 (WPA3), the latest security certification for 802.11 standards, has recently been shown to be vulnerable to several attacks. In this paper, we first describe the attacks on WPA3 networks that have been reported in prior work; additionally, we show that a deauthentication attack and a beacon flood attack, known to be possible on a WPA2 network, are still possible with WPA3. We launch and test all the above (a total of nine) attacks using a testbed that contains an enterprise Access Point (AP) and Intrusion Detection System (IDS). Our experimental results show that the AP is vulnerable to eight out of the nine attacks and the IDS is unable to detect any of them. We propose a design for a signature-based IDS, which incorporates techniques to detect all the above attacks. Also, we implement these techniques on our testbed and verify that our IDS is able to successfully detect all the above attacks. We provide schemes for mitigating the impact of the above attacks once they are detected. We make the code to perform the above attacks as well as that of our IDS publicly available, so that it can be used for future work by the research community at large.

Nadeem Akhtar, Malik M. Saad Missen

It is important to have multi-agent robotic system specifications that ensure correctness properties of safety and liveness. As these systems have concurrency, and often have dynamic environment, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play a major role in system correctness. Formal verification is used for exhaustive investigation of the system space thus ensuring that undetected failures in the behavior are excluded. We construct the system incrementally from subcomponents, based on software architecture. The challenge is to develop a safe multi-agent robotic system, more specifically to ensure the correctness properties of safety and liveness. Formal specifications based on model-checking are flexible, have a concrete syntax, and play vital role in correctness of a multi-agent robotic system. To formally verify safety and liveness of such systems is important because they have high concurrency and in most of the cases have dynamic environment. We have considered a case-study of a multi-agent robotic system for the transport of stock between storehouses to exemplify our formal approach. Our proposed development approach allows for formal verification during specification definition. The development process has been classified in to four major phases of requirement specifications, verification specifications, architecture specifications and implementation.

Nadeem Akhtar, Yann Le Guyadec, Flavio Oquendo

One of the most challenging tasks in specification engineering for a multi-agent robotic system is to formally specify and architect the system, especially as a multi-agent robotic system is concurrent having concurrent processing, and often having dynamic environment. The formal requirement and architecture specifications along with step-wise refinement from abstract to concrete concepts play major role in formalizing the system. This paper proposes the formal requirement and architecture specifications aspects of an approach that supports analysis with respect to functional as well as non-functional properties by step-wise refinement from abstract to concrete specifications and formal architecture definition. These formal specifications have been exemplified by a case study. As formal specification techniques are getting more mature, our capability to build a correct complex multi-agent robotic system also grows quickly.

Nadeem Akhtar

One of the most challenging tasks in software specifications engineering for a multi-agent system is to ensure correctness. As these systems have high concurrency, often have dynamic environments, the formal specification and verification of these systems along with step-wise refinement from abstract to concrete concepts play major role in system correctness. Our objectives are the formal specification, analysis with respect to functional as well as non-functional properties by step-wise refinement from abstract to concrete specifications and then formal verification of these specifications. A multi-agent system is concurrent system with processes working in parallel with synchronization between them. We have worked on Gaia multi-agent method along with finite state process based finite automata techniques and as a result we have defined the formal specifications of our system, checked the correctness and verified all possible flow of concurrent executions of these specifications. Our contribution consists in transforming requirement specifications based on organizational abstractions into executable formal verification specifications based on finite automata. We have considered a case study of our multi-agent system to exemplify formal specifications and verification.

Nadeem Akhtar, Anique Akhtar

The analysis, design and development of a graphical programming IDE for mini-robotic agents allows novice users to program robotic agents by a graphical drag and drop interface, without knowing the syntax and semantics of the intermediate programming language. Our work started with the definition of the syntax and semantics of the intermediate programming language. The major work is the definition of grammar for this language. The use of a graphical drag and drop interface for programming mini-robots offers a user-friendly interface to novice users. The user can program graphically by drag and drop program parts without having expertise of the intermediate programming language. The IDE is highly flexible as it uses xml technology to store program objects (i.e. loops, conditions) and robot objects (i.e. sensors, actuators). Use of xml technology allows making major changes and updating the interface without modifying the underlying design and programming.

Nadeem Akhtar, Aisha Shafique Ghori, Nadeem Salamat

This paper presents an approach based on the analysis, design, and formal verification of a multi-agent based university Information Management System (IMS). University IMS accesses information, creates reports and facilitates teachers as well as students. An orchestrator agent manages the coordination between all agents. It also manages the database connectivity for the whole system. The proposed IMS is based on BDI agent architecture, which models the system based on belief, desire, and intentions. The correctness properties of safety and liveness are specified by First-order predicate logic.