Donanım tasarlama dilinin birbirine karışmamışlık özelliğini doğrulayan araç

Donanım tanımlama dilleri giderek daha yüksek seviye özellikleri bünyelerinde barındırmaya başladı. Yüksek seviye programlamanın getirdiği esneklik ile donanım tasarımcıları obje tabanlı programlama ve fonksiyonel programlama gibi programlama paradigmalarından faydalanıp, dizayn sürelerini kısalttılar. Donanım tasarımlarının yüksek seviyeye geçmesi bu tasarımların veri akışı güvenliklerinin doğrulanmasında bir takım yeni sorunlar üretti. Bu çalışma yüksek seviye bir donanım tanımlama dilini genişleterek, ortaya çıkan bu yeni sorunların nasıl çözüleceğini ve bu sayede tasarımlarda veri sızmasının nasıl önüne geçilebileceğini göstermektedir. SecChisel (Chisel üzerine temellendirilmiş) veri akışı güvenliği özelliklerinden birbirine karışmamışlık (noninterference) özelliği kanıtlanabilir devreler tasarlanmasına imkan sunar. SecChisel ara değişken yaratılımı ve bu değişkenlere kademeli olarak aktarılması gerekilen güvenlik etiketleri gibi sorunları çözer. Bu sorunlar sadece kullanılan ana dilin direkt bir devre sentezlemesi yerine başka bir orta seviye dile çıktı vermesine özel durumlardır. SecChisel'ın devre veri akışı güvenliğini doğrulama yöntemi, devreyi bir takım dönüştürmelerden geçirip SMT çözücü formatında tekrar modellemektir. SecChisel'ın veri akışı güvenliğini derleme süresinde ve her hangi bir ek yük getirmeden doğrulayabildiği dizayn edip test etmiş olduğumuz devreler ile kanıtlanmıştır