Modern teknolojinin temelinde yer alan donanım platformları her geçen gün daha karmaşık hale gelirken, bu durum sistem programcıları için ciddi zorluklar yaratıyor. Donanım bileşenlerinin doğru programlanması ve güvenliğinin sağlanması, prose halinde yazılmış, eksik ve hatalı belgeler nedeniyle giderek zorlaşıyor.
Bu soruna çözüm bulmak için araştırmacılar, donanım semantiğini, yazılım davranışı varsayımlarını ve güvenlik özelliklerini tanımlamak üzere özel olarak tasarlanmış Sockeye adlı domain-spesifik bir programlama dili geliştirdi. Bu dil, donanım belgelerinin makine tarafından okunabilir hale getirilmesini ve matematiksel analiz yapılmasını mümkün kılıyor.
Araştırma ekibi, sekiz farklı donanım platformunun referans kılavuzlarından yola çıkarak makine tarafından okunabilir spesifikasyonlar oluşturdu ve bu platformların güvenlik durumlarını formal olarak kanıtladı. Bellek gizliliği ve bütünlüğü konularındaki güvenlik kanıtlarının yanı sıra, belgelerdeki çeşitli hataları da tespit ettiler.
En önemlisi, analizler sırasında gerçek dünyada kullanılan bir sunucu çipinde güvenlik açığı keşfedildi. Bu açık, üretici firma tarafından doğrulandı ve yaygın olarak kullanılan ağ cihazlarının geniş bir ailesini etkilediği belirlendi. Bu keşif, donanım güvenliği analizinde formal yöntemlerin ne kadar değerli olabileceğini gösteriyor.