Midlands Graduate School 2017

9 - 13 April, 2017

Lightning Talks

Modeling and Verification of Stealth Attacks on Security Protocols - Rajiv Ranjan Singh

Security protocols claim to provide security guarantees to end users while transacting online even in the presence of a powerful adversary. The advancement in technology has led to better secure protocols replacing their vulnerable predecessors. Attackers have also come up with newer classes of attacks on security protocols to exploit the vulnerabilities present. This situation challenges the protocol designers to design better protocols, historically an arduous task. The famous Needham-Schroeder public key protocol was broken and fixed after 17 years.

Protocol designers employ many techniques from testing and modeling to formal verification of security properties. They also perform conformance tests to make sure that the protocol implementations adheres to specifications and hence less likely to be attacked. One of the classes of attacks which is both hard to find and model is stealth attack. A stealth attack on a security protocol is an attack which does not alter the normal run of the protocol and hence harder to detect. To detect these attacks, we need to first develop a formal model to define and detect the stealth attacks. In this work, we will study the behaviour of security protocols under attacks and verify various security guarantees. Apart from studying the logs, we will use a mix of manual analysis and protocol verification tools such as TAMARIN Prover for the purpose. We look forward to proposing various techniques of identifying stealth attacks, including preparing a framework for separating stealth attacks from non-stealth attacks.


Agile Effort Estimation - Natasha Nigar

Software projects that are over-budget, delivered late, and fall short of users’ expectations have been a challenge in software engineering for decades. The success or failure of a software project heavily depends on the accuracy of effort estimation. The software project cost is primarily estimated based on effort which is defined as the time taken by the software development team members for individual tasks completion. Therefore, accurate effort estimation has gained highest importance due to exponential growth of large scale software applications. This research contributes by presenting a novel approach for effort estimation in ‘Agile Software development’ (ASD). In ASD, changes in customer requirements are proactively incorporated while delivering software projects within budget and time. We shall formulate effort estimation as the search-based problem and use computational intelligence techniques, such as evolutionary algorithms, to address following limitations in the current research for agile effort estimation.

  1. Datasets used for effort estimation contain single company projects data. We will use cross-company data to validate our model.
  2. Other than scrum and XP no other agile method was investigated. We will use KANBAN agile method in our research.
  3. We will be first to use line of code (LOC) as size metric.

The benefit of this research is that it will reduce the risk of software project falling behind schedules by providing realistic estimation figures.


Compositional Game Theory - Mirzhan Irkegulov

Classical game theory revolutionised the field of economics. However as it is now it is not scalable, because it lacks a notion of compositionality. For example, what does it mean to compose two prisoners' dilemmas? How would we build a larger game from smaller components? For a computer scientist, however, compositionality is natural. How would computer science bring new insights in modeling game-theoretic situations? Here, we explore the recent work on compositional game theory, its possibilities and limitations in modeling classical game theory. We will discuss how to attain the goal of implementing classical game theory in the compositional framework, and how category theory and functional programming can help.


A primer on guarded recursion - Christian Graulund

Guarded recursion provides an convenient way to work with infinite data streams and other co-algebraic structures. It allows us to do strong productivity checking on the type level, while still allowing us to work with data in a natural way.
I briefly present the later modality and show how this allows us to do guarded recursion and how productivity is checked for simple function streams.