​

COE/ICS Graduate Seminar

Seminar 1

An Executable Formal Framework for

Regular String Transformation in Rewriting Logic

by

Shadi Ayman AlHaj

Wednesday, April 26, at 4 pm

Room 22-119

​Abstract

Finite strings constitute a fundamental data type found in most general purpose programming languages. Furthermore, regular string transformations, which are a class of functions on finite strings, are widely used and have various applications in security, bioinformatics, etc. Given the ubiquity of regular string transformation and their importance, it would be useful to formally reason about these transformation at a high-level of abstraction that is close to the application in which they are used.

In this work, we develop formal framework based on rewriting logic and Maude in which regular string transformation can be formally specified and analyzed. The framework is executable enabling different types of formal analysis including simulations, inductive theorem proving and reachability analysis for both deterministic and non-deterministic regular string transformation.  We followed two complementary approaches in the thesis: one theoretical, in which formal semantics of the DReX language is developed, a language for describing regular string transformations, and the other is experimental in which a corresponding executable specification in Maude is developed and used for formal analysis. As a result, we have developed: (i) an algebraic deterministic semantics of DReX in Maude, and (ii) an extended rewriting semantics of a non-deterministic generalization of DReX capturing non-deterministic regular string transformation. The approach is illustrated using several real-world examples and case studies.

Shadi Ayman Alhaj is a master student in Information & Computer Science Department at King Fahd University of Petroleum & Minerals. He received his BSc degree in Computer Science from Hashemite University, Jordan. His current areas of interest include: Programming Language, Formal Specification, Security and Image Processing.   

Seminar 2

Monitoring System Calls in Virtualized Environment

by

Mustafa Ghaleb

Wednesday, April 26, at 3:30 PM

Building 22, Room 119

Abstract:

In computing, a system call is a programmatic way in which a computer program requests a service from the kernel of the operating system it is executed on. A program is usually limited to its own address space so that it cannot access other running programs or the operating system itself, and is usually prevented from directly manipulating hardware devices. System calls are made available by the OS to provide well-defined, safe implementations for such operations. In a virtualized environment, it’s crucial to provide protection for valuable assets within each virtual machine against unknown or new attacks. There are two main approaches to achieving this. First, install monitoring software in each virtual machine, which can report on processes by identifying used system calls and assets running within that virtual machine. The downside to this approach is that malicious processes running within the host might change their behavior because they can know that they are being monitored. Second, install monitoring software in the hypervisor and monitor all virtual machines managed by it. This approach is better than the first one because a malicious process running on any virtual machine can’t know it’s being monitored, in addition to being able to monitor all VMs managed by the hypervisor. We introduce a case study to monitor a system call in virtualized environment.