Concern-specific specification and verification to improve software quality and security

Project supervisors: Frank Piessens, Wouter Joosen, Pierre Verbaeten

Researchers: Lieven Desmet, Bart Jacobs, Jan Smans, Dries Vanoverberghe

Formal methods have long been recognized as an important tool to help ensure quality of software. In this research track we focus on the use of formal specification and verification techniques to eradicate certain classes of bugs. Examples of the classes of bugs that we target are concurrency related bugs and security related bugs.

Our approach consists of the design of concern-specific annotations, whose formal semantics is defined by translation to existing general-purpose specification languages such as Spec# and JML. If the translated program + specification verifies, we show that the original annotated program does not exhibit a specific type of erroneous behavior.

We have instantiated this idea in three different settings:

1. to deal with concurrency related bugs (data races and deadlocks), as described in detail in the following papers:
   • B. Jacobs, K. R. M. Leino, F. Piessens, and W. Schulte, Safe concurrency for aggregate objects with invariants, Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (Aichernig, B.K. and Beckert, B., eds.), pp. 137-146, 2005
   • B. Jacobs, J. Smans, F. Piessens, and W. Schulte, A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. To be presented at the Eighth International Conference on Formal Engineering Methods (ICFEM 2006), Macau, October 29-November 3, 2006.
     
2. to deal with stack-inspection based sandboxing related bugs, as described in detail in the following papers:
   • J. Smans, B. Jacobs, and F. Piessens, Static Verification of Code Access Security Policy Compliance of .NET Applications, Journal of Object Technology 5 (3), pp. 35-58, April, 2006.
   • J. Smans, B. Jacobs, and F. Piessens, Static verification of code access security policy compliance of .NET applications, Proceedings of the 3rd International Conference on .NET (Skala, V. and Nienaltowksi, P., eds.), pp. 1-12, 2005
     
3. to deal with data dependency related bugs as described in detail in the following papers:
   • L. Desmet, F. Piessens, W. Joosen, and P. Verbaeten, Static Verification of Indirect Data Sharing in Loosely-coupled Component Systems. In SC 2006, (W. Löwe and M. Südholt, eds.), vol. 4089/2006, Lecture Notes in Computer Science, Springer-Verlag Berlin Heidelberg, 2006, pp.34-49.
   • L. Desmet, F. Piessens, W. Joosen, and P. Verbaeten, Bridging the Gap Between Web Application Firewalls and Web Applications. Accepted at Formal Methods in Security Engineering (FMSE'06), November 3, Alexandria, Virginia, USA.