Dr Antonio Cau

Job: Senior Research Fellow

Faculty: Technology

School/department: School of Computer Science and Informatics

Research group(s): Software Technology Research Laboratory

Address: De Montfort University, The Gateway, Leicester, LE1 9BH, United Kingdom

T: +44 (0)116 257 7937

E: cau@dmu.ac.uk

W: www.dmu.ac.uk

 

Personal profile

Dr. Antonio Cau gained his MSc in Computer Science from Eindhoven University of Technology (The Netherlands). He then joined Christian Albrechts University of Kiel (Germany) as a junior lecturer where he was awarded his PhD. He subsequently worked as a Research Associate on the EPSRC project `A Compositional Approach to the Specification of Systems using ITL and Tempura'. Dr. A. Cau is currently a University Senior Research Fellow at the Software Technology Research Laboratory, De Montfort University.

Dr. Cau's main interests are the compositional verification and specification of critical systems using formal methods. He has developed several tools (AnaTempura, FLCheck) that can be used to accomplish this task.

Research group affiliations

Software Technology Research Laboratory (STRL)

Publications and outputs 

  • A Novel Approach to Worm Detection Systems
    A Novel Approach to Worm Detection Systems Al-Saawy, Yazed B.; Siewe, Francois; Cau, A. (Antonio) Computer worms are a type of malicious malware that prey on networked machines. A number of different detection mechanisms have been presented in the literature to detect worms. However, a common drawback of these mechanisms is that any failure to detect the worms results in damaging the real machines. This study proposes a new approach to detection that goes beyond the currently available signature and behavior-based approaches. In contrast to the traditional worm detection system (𝑊𝐷𝑆) that use signature and behavior-based approaches, our proposed approach is based on detection by the damage caused by worms on dummy machines rather than the real machines. The proposed 𝑊𝐷𝑆 adds additional security as compared to the currently used systems by allowing worms to conduct their normal behavior in a dummy host, thus protecting the rest of the network from damage. The proposed 𝑊𝐷𝑆 was designed within a network setting and was capable of sending and receiving files and messages between hosts as part of the overall detection mechanism.
  • Runtime-Monitoring for Industrial Control Systems
    Runtime-Monitoring for Industrial Control Systems Janicke, Helge; Nicholson, Andrew; Webber, S.; Cau, A. (Antonio)
  • Verification and enforcement of access control policies
    Verification and enforcement of access control policies Cau, A. (Antonio); Janicke, Helge; Moszkowski, B. C.
  • Behavioural API based Virus Analysis and Detection
    Behavioural API based Virus Analysis and Detection Al Amro, S.; Cau, A. (Antonio) The growing number of computer viruses and the detection of zero day malware have been the concern for security researchers for a large period of time. Existing antivirus products (AVs) rely on detecting virus signatures which do not provide a full solution to the problems associated with these viruses. The use of logic formulae to model the behaviour of viruses is one of the most encouraging recent developments in virus research, which provides alternatives to classic virus detection methods. To address the limitation of traditional AVs, we proposed a virus detection system based on extracting Application Program Interface (API) calls from virus behaviours. The proposed research uses a temporal logic and behaviour-based detection mechanism to detect viruses at both user and kernel level. Interval Temporal Logic (ITL) will be used for virus specifications, properties and formulae based on the analysis of API calls representing the behaviour of computer viruses.
  • Formalising of transactional memory using interval temporal logic (ITL)
    Formalising of transactional memory using interval temporal logic (ITL) El-kustaban, Amin Mohammed Ahmed; Moszkowski, B. C.; Cau, A. (Antonio)
  • A framework for the detection and prevention of SQL injection attacks
    A framework for the detection and prevention of SQL injection attacks Shafie, E.; Cau, A. (Antonio)
  • Specification analysis of transactional memory using ITL and AnaTempura
    Specification analysis of transactional memory using ITL and AnaTempura El-kustaban, Amin Mohammed Ahmed; Moszkowski, B. C.; Cau, A. (Antonio)
  • Dynamic Access Control Policies - Specification and Verification
    Dynamic Access Control Policies - Specification and Verification Janicke, Helge; Cau, A. (Antonio); Siewe, Francois; Zedan, Hussein Security requirements deal with the protection of assets against unauthorized access (disclosure or modification) and their availability to authorized users. Temporal constraints of history-based access control policies are difficult to express naturally in traditional policy languages. We propose a compositional formal framework for the specification and verification of temporal access control policies for security critical systems in which history-based policies and other temporal constraints can be expressed. In particular, our framework allows for the specification of policies that can change dynamically in response to time or events enabling dynamic reconfiguration of the access control mechanisms. The framework utilizes a single well-defined formalism, interval temporal logic, for defining the semantics of these policies and to reason about them.We illustrate our approach with a detailed case study of an electronic paper submission system showing the compositional verification of their safety, liveness and information flow properties.
  • Behaviour-based virus detection system using interval temporal logic.
    Behaviour-based virus detection system using interval temporal logic. Al Amro, S.; Cau, A. (Antonio)
  • The Calculus of context-aware ambients.
    The Calculus of context-aware ambients. Siewe, Francois; Zedan, Hussein; Cau, A. (Antonio) We present the Calculus of Context-aware Ambients (CCA in short) for the modelling and verification of mobile systems that are context-aware. This process calculus is built upon the calculus of mobile ambients and introduces new constructs to enable ambients and processes to be aware of the environment in which they are being executed. This results in a powerful calculus where both mobility and context-awareness are first-class citizens. We present the syntax and a formal semantics of the calculus. We propose a new theory of equivalence of processes which allows the identification of systems that have the same context-aware behaviours. We prove that CCA encodes the π-calculus which is known to be a universal model of computation. Finally, we illustrate the pragmatics of the calculus through many examples and a real-world case study of a context-aware hospital bed.

Click here to view a full listing of Antonio Cau's publications and outputs.

Research interests/expertise

Verification and specification of critical systems using maths and logic

Areas of teaching

Software Engineering

Qualifications

PhD, (Kiel, Germany)

MSc, (Eindhoven, The Netherlands)

Courses taught

Rigorous Systems

Formal Methods Engineering

Membership of professional associations and societies

IEEE

ACM

KIVI

Current research students

First supervisor for:

Sami Alsarhani
Yazed Alsaawy
Emad Shafie
Bader Alouffi
David Smallwood
Sulaiman Al Amro

 

Second supervisor for:

Laila Alhimale
Salem Almarri
Adeeb Ali Alnajjar
Khaled Alodadi
Fahad Alqahtani
Ali Mousa G Alzahrani
Abdullah Dabil

Externally funded research grants information

Project Title: Trust Management in Collaborative Systems (aToMICS)
Funded By: Defence Technology Centre in Data and Information Fusion DIF-DTC (MoD, QinetiQ)
Start Date: 1st October 2006
End Date: 31st March 2009
Role: Project manager
Collaborators: Members of the DIF-DTC consortium: BT, QinetiQ, General Dynamics, Imperial College and the Universities of Bristol, Cardiff, Cambridge, Southampton, De Montfort, Surrey and Cranfield.

Professional esteem indicators

Journal reviews:

2012, Transactions on Computational Logic
2012, Journal of Logic and Algebraic Programming
2011, Journal of Computer Science and Technology
2011, Control Engineering Practice
2010, Software and System Modeling (SoSyM) journal
2010, Formal Methods in System Design
2009, Fundamenta Informaticae
2008, Formal Aspects of Computing
2008, Journal of Systems and Software
2008, Journal of Zhejiang University-SCIENCE A
2008, Control Engineering Practice

Conference reviews:

TIME 12, 12-14 September, PC member, Organizing committee member and reviewer
SANES 2012, 24 - 26 February, 2012: PC member and reviewer
AEECT 2011, 6-8 December: PC member and reviewer
Casemans 2011, 17-21 September: PC member and reviewer
TIME11, 12-14 September: PC member and reviewer
Informatics 2011, 20 - 22 July: PC member and reviewer
LATA2011, 26-31 May: reviewer
Casemans 2010, 26-29 September: PC member and reviewer
CSL 2010, 23 - 27 August: reviewer
Informatics 2010, 26 - 28 July: PC member and reviewer
Informatics 2009, 17 - 19 June: PC member and reviewer
YRSOC 2008, 12- 13 June: PC member and reviewer
SEFM-08, 10 - 14 November: reviewer

Search Who's Who

 
News target area image
News

DMU is a dynamic university, read about what we have been up to in our latest news section.

Events target area image
Events

At DMU there is always something to do or see, check out our events for yourself.

Mission and vision target area image
Mission and vision

Read about our mission and vision and how these create a supportive and exciting learning environment.