Generating runtime verification specifications based on static code analysis alerts

Abstract

Yazılım hatalarının bulunması amacıyla kullanılan birçok yöntem bulunmaktadır. Buyöntemlerden biri olan statik kod analizi koddaki hataların, kodun çalıştırılmadanortaya çıkarılmasını sağlamaktadır. Bunu tamamlayıcı nitelikte olan çalışma zamanıdoğrulama ise dinamik sistem davranışlarını yazılmış olan kurallara göre kontrol etmek için kullanılmaktadır. Bu kural listesi genellikle sistem gereksinimleri ve kısıtlarına göre manuel olarak oluşturulmaktadır. Bu tezde, statik kod analizi araçlarınınoluşturduğu uyarılardan çalışma zamanı doğrulama kurallarını otomatik olarak oluş-turan yeni bir yöntem ve araç geliştirilmiştir. Alana özgü bir dil geliştirilerek, uyarıtiplerine özgü kurallar tanımlanması sağlanmıştır. Oluşturulan bu kuralların ihlaledilip edilmediğine göre hatanın gerçekleşip gerçekleşmediğine karar verilmektedir.Çalışma zamanı doğrulama kuralları her bir uyarı için daha önceden tanımlanmış kurallara göre otomatik oluşturulmaktadır. Daha sonra ise, oluşan bu kurallara ilişkinçalışma izleyiciler otomatik sentezlenerek, sisteme entegre edilmektedir. Bu izleyiciler yazılımla birlikte çalışarak tespit edilen hataları ve yanlış üretilmiş uyarılarıraporlamaktadır. Bir kere oluşturulan kurallar farklı projelerde kullanılabilmektedir.Bu durumu gösterebilmek için iki farklı açık kaynak kod üzerinde vaka çalışmalarıgerçekleştirilmiştir. Aracımız şu anda Java programlama dili için uyarı üreten ikifarklı statik kod analiz aracını desteklemektedir. Ayrıca bu araç, yeni statik kodaraçlarını destekleyebilecek şekilde tasarlanmıştır.

There are various approaches in order to find bugs in a software system. One ofthese approaches is static code analysis, which tries to achieve this goal by analyzingcode without executing it. Another complementary approach is runtime verification,which is employed to verify dynamic system behavior with respect to a set of specifications at runtime. These specifications are often created manually based on systemrequirements and constraints. In this thesis, we propose a novel methodology andtool support for automatically generating runtime verification specifications based onalerts that are reported by static code analysis tools. We introduce a domain specific language for defining a set of rules to be checked for an alert type. Violationsof the rules indicate either the absence or existence of an actual bug designated bythe instances of that alert type. Formal verification specifications are automaticallygenerated for each reported alert instance based on the defined rules. Then, runtimemonitors are automatically synthesized and integrated into the system. These monitors report detected errors or false positive alerts during software execution. Theset of rules can be reused across different projects. We performed case studies withtwo open source software systems to illustrate this. Our tool currently supports theuse of two different static code analysis tools for generating runtime monitors in Javalanguage. It is designed to be extendible for supporting other tools as well.