Yazılım güvenliği alanında önemli bir gelişme yaşandı. Araştırmacılar, hafıza manipülasyonu yapan programlarda karmaşık güvenlik özelliklerini doğrulayabilen ilk mantık sistemi olan Hyper Separation Logic'i (HSL) geliştirdi.
Yazılımlarda non-interference, determinizm ve genelleştirilmiş non-interference gibi kritik güvenlik özellikleri hiperproperties olarak adlandırılıyor. Bu özellikler, bir programın birden fazla çalışma senaryosunu karşılaştırarak değerlendiriliyor. Mevcut separation logic sistemleri sadece belirli hiperproperties sınıflarını analiz edebiliyordu, ancak quantifier alternation gerektiren özellikleri desteklemiyordu.
HSL, bu sınırlamayı aşan ilk sistem olma özelliği taşıyor. Önceki tek alternatif olan Hyper Hoare Logic, heap manipülasyonu yapan programları desteklemediği için modern imperativ programlarda kullanılamıyordu. Bu durum, günlük yazılım geliştirmede büyük bir boşluk yaratıyordu.
Yeni sistem, modüler reasoning yaklaşımını destekleyerek, karmaşık güvenlik özelliklerinin parça parça analiz edilmesine olanak tanıyor. Bu özellik, büyük ölçekli yazılım projelerinin güvenlik analizinde önemli avantajlar sağlayacak.