Seminars

View all Seminars  |  Download ICal for this event

Verification of Timed Security Properties

Series: Department Seminar

Speaker: Nabarun Deka

Date/Time: Jul 18 11:30:00

Location: CSA Lecture Hall (Room No. 112, Ground Floor)

Abstract:
In this talk I will present two of my (ongoing and past) works on verifying security properties involving constraints on timings of events. In the first line of work, we study the problem of verifying security properties of real-time systems. Security properties of such systems often involve reasoning about multiple execution traces of the system (called hyper-properties) as opposed to a single trace of the system or a tree of executions. Examples of such properties include information flow, side channel attacks, and service-level agreements. We present a branching time specification logic, HCMTL*, for such hyperproperties and study the problem of verifying a system represented by a timed automaton against a HCMTL* specification. We show that the problem is undecidable, and becomes decidable if we consider executions up to a fixed time horizon T.

The second line of work studies insecurity of timed security protocols. Several protocols, such as distance bounding protocols, require reasoning about timings of messages to ensure security. Such protocols are always insecure against a standard omnipotent and omnipresent Dolev-Yao attacker model. We introduce a suitable attacker model for timed protocols and study the problem of verifying security of timed protocols against this attacker model. We show that, like the untimed case, insecurity for timed protocols is NP-complete.

Speaker Bio:
Nabarun Deka is a PhD student in the Computer Science Department at the University of Illinois Urbana-Champaign. Before starting his PhD, he completed his BS and MS in Mathematics at the Indian Institute of Science. His research interests lie in applying techniques from formal methods to study verification problems in computer security.

Host Faculty: Deepak DSouza