laboratory of security systems formalism

laboratory of security systems formalism

Mehran S.Fallah

  • Introduction

 

 

 

 

 

 

 

Overview (History, motivation, outstanding features)

 

History:

The Formal Security Lab (FSL) commenced its activities in 2006as a research and development centertargeted at ingenious M.Sc. and Ph.D. students. The laboratory mainly focuses on the use of formal techniques in the design and analysis of security systems and mechanisms. This laboratory provides an opportunity for meticulous understanding and examining fundamental and core theories in the realm of information security. In particular, the members of the lab are currently working on security by construction through which system development tools are so designed that the products have built-in security mechanisms and enforce security policies automatically. More specifically, the main theme is language-based security.  

 

Motivation:

Computer systems are widely threatened by insecure software. In recent years, the computer science community has led to the conclusion that informal methods are not enough for secure system development and the best way to have a provable secure system is the use of formal techniques, especially when they are employed methodically to embed security mechanisms into the code.  This has motivated scholars of the AUT to establish a lab to undertake the studies in the field of security by construction through formal techniques.

 

 

Outstanding features:

The knowledge and experience provided through thelab enables security scholars to build robust secure systems by the employment of the state-of-the-art techniques in the area of formal methods and language-based security.

 

 

 

 

 

Research focus/goals:

1-   Formalizing recent results in information security as an essential step in converting the craft of information security to a science.

2-   Constructing provable secure systems through the foundations of programming languages.

3-   Extending current tools and techniques for the formal design and analysis of security mechanisms so that they can cover new areas.

 

 

 

 

Equipments:

High-performance computers, tools for the formal analysis of security protocols, general-purpose tools for model checking and theorem proving

 

 

Research projects:

Research projects in FSL are divided into two main categories: projects in Language-based Security and those in Game Theoretic approaches to security. The former involves three principal disciplines known as static enforcement, run-time mechanisms, and program rewriting. The high-level titles of current FSL projects are

-         Information flow security by securitytype-systems

-         Semantics of Information flow security

-         Theoretical issues of policy enforcement through  program rewriting

-         The interaction between logic and programming languages theory and its use in the design of and reasoning about security protocols

-         Game theory and adversarial learning

 

 

People:

 

Supervisor

Prof. Mehran S. Fallah: Foundations for Information Security, Language-based Security, Logic, Game Theory

 

Honorary Member

Prof. Masoud Pourmahdian: Logic, Domain Theory, Denotational Semantics

 

Ph.D. Candidates

AfshinLamei: Formal Characterization of Security Policy Enforcement through Program Rewriting

 

Sharar Ahmadi: An Epistemic Temporal Logic for Verifying Authentication Protocols

 

BehnamSattarzadeh: Modeling and Type-based Analysis of Authentication Protocols in the Presence of Insider Attacks

 

ZeinabIranmanesh: Information Flow Security in Multithreaded Object-Oriented Programming

 

Ali Noorollahi: Nonmonotonic Logics and the Specification and Enforcement of Access Control Policies in Pervasive Computing Environments

 

M.Sc. Students

GoharShakoori: Quantified Information Flow Security in Object-Oriented Programming

 

Hossein Tehranifar: Game-Theoretic Analysis of Adversarial Learning

 

KooshanAbedian: Compositional Security in a Model Language for Java

 

Mahdi Fadaee: Automatic Enforcement of  User-defined Security Policies in Object-Oriented Programming

 

Alireza Siadat: Enforcing Flow-Insensitive Noninterference through Program Rewriting in a Model Language for Java

 

 

 

 

 

 

 

 

 

Recent Achievements :

 

The Tool Cryptyc+: An Extension of Cryptyc to Analyze Security Protocols in the Presence of Insider Attacks (The code and example analyses are available at the home page of the lab athttp://ceit.aut.ac.ir/formalsecurity/tasp/)

 

Is Cryptyc Able to Detect Insider Attacks? Proc. 8th Int. Workshop on Formal Aspects of Security and Trust (FAST 2011), Leuven, Belgium, Sept. 2011.

   
   
 

Reconstructing Security Types for Automated Policy Enforcement in FABLE. Proc. 5th Int. Conf. Network and System Security (NSS 2011), Milan, Italy, Sep. 2011, pp. 358-363.

   
   
 

A Distributed Client-Puzzle Mechanism to Mitigate Bandwidth Attacks. Proc. 5th Int. Conf. Network and System Security (NSS 2011), Milan, Italy, Sep. 2011, pp. 145-152.

   
   
 

 A Logical View of Nonmonotonicity in Access Control. Proc. Int. Conf. Security and Cryptography (SECRYPT 2011), Seville, Spain, July. 2011.

   
   
 

 A Game-Based Sybil-Resistant Strategy for Reputation Systems in Self-Organizing MANETs, The Computer Journal, Oxford Univ. Press, Vol. 54, No. 4, pp. 537-548, 2011.

   
   
 

 A Puzzle-Based Defense Strategy Against Flooding Attacks Using Game Theory. IEEE Trans. Dependable and Secure Computing, Vol. 7, No. 1, pp. 5-19, 2010.

   
   
 

 A Secure Credit-Based Cooperation Stimulating Mechanism for MANETs Using Hash Chains. Future Generation Computer Systems, Vol. 25, No. 8, pp. 926-934, 2009.

   
   
 

 HWSC: A Fully Automatic Web Services Composer. Proc. 2009 Euro-American Conf. Telematics, Prague, Czech, Jul. 2009.

   
   
 

 A Game-Theoretic Cooperation Stimulus Routing Protocol in MANETs. IAENG Int. Journal of Computer Science, Vol. 35, No. 1, pp. 174-181, 2008.

   
   
 

Service Availability in Concurrent Systems - Part I: A theory of Hierarchical Services of Interacting Processes. The Computer Journal, Oxford. Univ. Press, Vol. 50, No. 5, pp. 522-534, 2007.

   
   
 

 Service Availability in Concurrent Systems - Part II: Analysis and Case Studies Using HSIP. The Computer Journal, Oxford Univ. Press, Vol. 50, No. 5, pp. 535-554, 2007.

   
   
 

Stimulating Cooperation in MANETs Using Game Theory. Proc. 2007 Int. Conf. Wireless Networks, London, UK, Jul. 2007. (Certificate of Merit Winner)