Muhammad Taimoor Khan, MSc. PhD. | 29.02.2016 | 11:00 Uhr | E.2.69

Abstract

In this talk, we present a rigorous behavior based approach to develop reliable, secure and resilient application software for industrial control systems (in particular). The goal here is to employ formal methods to first build application right and then to continuously monitor the application for security and resilience.
To achieve the goal, we first develop correct-and-secure-by-construction application software using theorem proving (i.e. prover Coq) through refinement and synthesis of abstract data types. Then we introduce a run-time security monitor for application software, which detects both known and unknown computational cyber attacks. For resilience, we employ dependency directed reasoning to recover the system in a safe state, if any inconsistency is detected. Our security monitor is sound and complete, eliminating false alarms, as well as efficient, supporting real-time systems. In contrast, conventional run-time security monitors for application software either produce (high rates of) false alarms (e.g. intrusion detection systems) or limit application performance (e.g. run-time verification systems).
Our run-time monitor detects attacks by checking the consistency between the application run-time behavior and its expected behavior modeled in its specification. Our specification language is based on monadic second order logic (i.e. first order logic and set theory) and event calculus interpreted over algebraic data structures; application implementation can be in any programming language. Based on our defined denotational semantics of the specification language, we prove that the security monitor is sound and complete, i.e. it produces an alarm if and only if it detects an inconsistency between the application execution and the specified behavior. Importantly, the monitor detects not only cyberattacks but all behavioral deviations from specification, e.g. bugs, and so, is readily applicable to the security of legacy systems.
Finally, we present the evaluation of the monitor in the industrial control systems security domain, specifically in water management, demonstrating that run-time, sound and complete monitors employing verification techniques are effective, efficient and readily applicable to demanding real-time critical systems, without scalability limitations.

Muhammad Taimoor Khan is a postdoctoral researcher at Qatar Computing Research Institute (jointly with CSAIL, MIT, USA), Qatar. His current research is to develop reliable, secure and resilient software by the application of formal methods. On one hand, his project is focused on developing a tool to automatically detect and correct, known and unknown attacks through monitoring behavioral inconsistencies between specification and execution at run-time. On the other hand, his another project is focused on using theorem prover as a programming language to develop correct-and-secure-by construction software.
Prior to this, Taimoor Khan has passed doctoral studies at Research Institute for Symbolic Computation, Hagenberg, Austria with All-Distinctions in 2014. His PhD dissertation was about formal specification and verification of computer algebra software. Before joining RISC, he graduated in MSc Advanced Distributed Systems from the University of Leicester, UK with Distinction in 2008. As a final semester project he worked on the model-based verification of the various communication protocols of NASA in the frame of project “Space Link Extension Service Management”. Also prior to this, he completed his M.Sc. in Computer Science from Pakistan in 2001 and then worked for about five years in the software industry specializing in Java (EE/ME), XML and Web Services.
Taimoor Khan has been visiting scientist at various international reputed institutes including CSAIL, MIT, USA and ENSIIE, INRIA, France. Also he has won various research awards including the best student paper award at the most premier conference in computer algebra (CICM) in 2012.
He is also working as an associate tutor at University of Leicester, UK. Here he is teaching different courses (e.g. Domain Specific Languages) to MSc students (DL) and supervising their final semester projects. Prior to that, he has also taught undergraduate and graduate students at numerous universities in Pakistan as an assistant professor for several years.

Faisal Z. Qureshi | 13.01.2016 | 10:00 Uhr | Seminarraum Lakeside Labs B4.1.114

Abstract:

We developed a new method for extracting 3D flight trajectories of droplets using high-speed stereo capture. We noticed that traditional multi-camera tracking techniques fare poorly on our problem, in part due to the fact that all droplets have very similar shapes, sizes and appearances. Our method uses local motion models to track individual droplets in each frame. 2D tracks are used to learn a global, non-linear motion model, which in turn can be used to estimate the 3D locations of individual droplets even when these are not visible in any camera. We have evaluated the proposed method on both synthetic and real data and our method is able to reconstruct 3D flight trajectories of hundreds of droplets. The proposed technique solves for both the 3D trajectory of a droplet and its motion model concomitantly, and we have found it to be superior to 3D reconstruction via triangulation. Furthermore, the learned global motion model allows us to relax the simultaneity assumptions of stereo camera systems. Our results suggest that, even when full stereo information is available, our unsynchronized reconstruction using the global motion model can significantly improve the 3D estimation accuracy.

Bio:

Faisal Qureshi is an Associate Professor of Computer Science at the University of Ontario Institute of Technology (UOIT), Oshawa, Canada. He obtained a PhD in Computer Science from the University of Toronto in 2007.  He also holds an M.Sc. in Computer Science from the University of Toronto, and an M.Sc. in Electronics from Quaid-e-Azam University, Pakistan.  Prior to joining UOIT, he worked as a Software Developer at Autodesk. His research interests include sensor networks, computer vision, and computer graphics. He has also published papers in space robotics.  He has interned at ATR Labs (Kyoto, Japan), AT&T Research Labs (Red Bank, NJ, USA), and MDA Space Missions (Brampton, ON, Canada).  He is a member of the IEEE and the ACM.

Alexander Beck | 10.12.2015 | 15:00 Uhr | HS 4

Kurzfassung

IT-Systeme sind stark zusammenhängende komplexe Strukturen, so dass eine Fokussierung auf das IT-System im Ganzen nur eine bedingt effiziente Sicherheitsbewertung gewährleistet. Die Sicherheit dieser komplexen Systemlandschaften stets aktualisiert unter Berücksichtigung aller Wechselbeziehungen zwischen Komponenten dieser Systemlandschaften darzustellen, gestaltet sich mangels geeigneter Modelle schwierig. Neben diesen Modellen bilden Schwachstellenbewertungen die Grundlage für die Bewertung der Sicherheit und werden durch aufwändige Betrachtungen interpretiert, um eine Gesamtbewertung zu ermitteln. Will man dieses Vorgehen automatisieren, muss zunächst eine gemeinsame Repräsentation von Schwachstellenbewertungen vereinbart werden. Das dazu geeignete Common Vulnerability Scoring System (CVSS) ermöglicht die Bewertung einzelner Schwachstellen hinsichtlich verschiedenster Fragestellungen. Um eine Darstellung der Gesamtsicherheit zu erreichen, müssen diese Schwachstellen aggregiert werden. Unter einer Aggregation ist dabei die gemeinsame Interpretation aller im Fokus stehenden Schwachstellen zur Erreichung einer Gesamtbewertung zu verstehen, welche auf Basis eines neuronalen Netzwerkes erfolgt. Das neuronale Netz ist ein lernfähiges Konzept der Informatik, mit dem es möglich ist auf Basis definierter Eingabeparameter ein definiertes Ergebnis zu modellieren. Dabei wird das Netz trainiert und die Ergebnisse mit Ergebnissen der bisherigen manuellen Bewertungsverfahren verglichen, bis eine entsprechende Qualität der automatisch ermittelten Ergebnisse gesichert ist.

Alexander Beck ist seit 2011 bei der Volkswagen AG tätig. Zuvor studierte er Informatik an Hochschule Harz und Otto-von-Guericke-Universität Magdeburg unter anderem mit den Schwerpunkten Datenintensive Systeme und Sicherheit. Im Rahmen seiner Dissertation erforscht er Verfahren zur automatisierten Sicherheitsbewertung von komplexen heterogenen IT-Infrastrukturen auf Basis neuronaler Netze.
Beruflich war er mehrere Jahre in der Informationssicherheit im Volkswagen Konzern tätig und beschäftigte sich mit den Themen Authentifizierung und Verschlüsselung. Aktuell arbeitet er im Bereich IT Projekt- und Programmmanagement der Volkwagen Financial Services AG und verantwortet IT Projekte im In- und Ausland.

Dr. Christian Beecks | 24.11.2015 | 16:00 Uhr | E.2.42

Abstract

With the advent of social networks and the advancement of powerful internet-enabled mobile devices, millions of users are able to easily generate, process, and share multimedia data at billion-scale every single day. The resulting multitude and versatility of multimedia data made available in the Internet challenge todays’ data management and analysis algorithms. In many research and application areas including information retrieval, data mining, and computer vision, users are no longer satisfied with keyword-based access but want to search, browse, explore, and analyze multimedia data according to content-based characteristics. One fundamental operation underlying many data analysis algorithms is similarity search which aims at retrieving the most similar multimedia objects with respect to a query. In order to carry out similarity search for query-like multimedia objects, the way of modeling similarity is of major significance due to its impact on efficiency and effectiveness.

In this talk, I will present my ongoing research in this fascinating field and highlight future research directions. More specifically, I will show how to approach similarity between multimedia data objects by means of gradient-based signatures in order to facilitate data analysis with high efficiency and efficacy.

Christian Beecks is a postdoctoral researcher in the data management and data exploration group at RWTH Aachen University, Germany. His research interests include efficient and adaptive multimedia data analysis, distance-based multimedia indexing and query processing, and real-time data management.