Research Interests


Research Interests 
I do research about security, in particular, access control. In my PhD, I developed/applied run-time reasoning and verification techniques for all activities involved in static and dynamic analysis of certain security properties and constraints. So simply, I work on run-time verification in access control. The access control model I consider is mainly Role Based Access Control (RBAC). Conventionally access control to resources has been considered from two perspectives: 
  • Model: How to model a system with a generic approach that has the necessary machinery to represent authorization requirements. Examples include, Role Based Access Control (RBAC) model,  Attribute Based Access Control (ABAC).
  • Specification: Expressive notations for encoding an access control policy.
Recent advances in automated reasoning enabled the use of formal methods in verification of the specifications at design time. However, as many information (i.e. parameter) used in access control decision is only available at run-time and the design time analysis can easily lead to state explosion problem in many access control settings, run-time analysis can provide efficient solutions to many verification problems. So the question is can we use the existing methods or develop new ones that exploit automated reasoning techniques at run-time?

What I do is developing and implementing formal/semi-formal methods for the verification of specifications at run-time by 1. Approximating some of the run-time parameters at compile time and simulation, 2. Using efficient representation techniques and algorithms to encode the problem, 3. Optimizing the analysis of state traces at run-time (in just in time manner) by state space elimination as at run-time one needs to deal with only finite traces.