Rewriting Logic Methods in Security: The DOS Case
Professor, Computer Science
University of Illinois, Urbana-Champaign
(Video runs from 00:17:00 to 01:10:30)
Rewriting logic is a computational logic ideally suited for modeling concurrent systems. Such models are executable in a language like Maude and can be formally analyzed by model checking and theorem proving methods. In particular, rewriting logic methods have been extensively used to model and analyze secure systems in areas such as:
- cryprographic protocols
- network security
- browser security
- access control, and
- code security
The talk will focus on the modeling and formal analysis of defense mechanisms against Denial of Service (DoS) attacks, where the systems, attackers and defenses are modeled by probabilistic rewrite rules, and the effectiveness of the defenses can be analyzed by statistical model checking.
"Twenty Years of Rewriting Logic"
"Probabilistic Modeling and Analysis of DoS Protection for the ASV Protocol"
"Stable Availability Under Denial of Service Attacks Through Formal Patterns"
José Meseguer received a Ph.D. in Mathematics from the University of Zaragoza, Spain. He is Professor of Computer Science at the University of Illinois at Urbana-Champaign (UIUC). Prior to moving to UIUC he was a Principal Scientist as the Stanford Research Institute (SRI), after having held postdoctoral positions at the University of California at Berkeley and IBM Research. He was also an Initiator Member of Stanford University's Center for the Study of Language and Information (CSLI).
Dr. Meseguer has made fundamental contributions in the frontier between mathematical logic, executable formal specification and verification, declarative programming languages, programming methodology, concurrency, and security. His work in all these areas, comprising over 300 publications, is very highly cited. The Maude language is one of the most advanced and efficient executable formal specification languages. It supports a wide range of formal analyses, including symbolic simulation, search, model checking, and theorem proving. It is also an advanced declarative concurrent language with sophisticated object-oriented features and powerful module composition and reflective meta-programming capabilities. He, his collaborators, and other researchers have used Maude and its tool environment to build sophisticated systems and tools, and to specify and analyze many systems, including cryptographic protocols, active network protocols, models of cell biology, executable formal semantics of programming languages, formal analyzers for conventional code, theorem provers, and tools for interoperating different formal systems. He has given numerous invited lectures at international scientific meetings and has taught advanced courses on his research at leading American, British, German, Spanish, Italian, and Japanese universities and research centers. He has also served in numerous program committees of international scientific conferences and as editor of various scientific journals.