A tool for verifying noninterference property for HDL

Abstract

Donanım tanımlama dilleri giderek daha yüksek seviye özellikleri bünyelerindebarındırmaya başladı. Yüksek seviye programlamanın getirdiği esneklik ile donanımtasarımcıları obje tabanlı programlama ve fonksiyonel programlama gibi programlamaparadigmalarından faydalanıp, dizayn sürelerini kısalttılar. Donanım tasarımlarının yüksekseviyeye geçmesi bu tasarımların veri akışı güvenliklerinin doğrulanmasında bir takım yenisorunlar ü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ş) veriakışı güvenliği özelliklerinden birbirine karışmamışlık (noninterference) özelliğikanıtlanabilir devreler tasarlanmasına imkan sunar. SecChisel ara değişken yaratılımı ve budeğ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 ortaseviye dile çıktı vermesine özel durumlardır. SecChisel'ın devre veri akışı güvenliğinidoğrulama yöntemi, devreyi bir takım dönüştürmelerden geçirip SMT çözücü formatındatekrar modellemektir. SecChisel'ın veri akışı güvenliğini derleme süresinde ve her hangibir ek yük getirmeden doğrulayabildiği dizayn edip test etmiş olduğumuz devreler ilekanıtlanmıştır

Hardware description languages started to adopt high-level functionalities. Through theflexibility of high-level programming, hardware designers can leverage object-orientedprogramming and functional programming paradigms to specify the hardware for quickerdesign time. This transition to high-level hardware descriptions created a new set ofproblems about verifying their noninterference property. By extending a high-level HDL,this thesis shows how to approach and solve this new set of problems and thus preventinginformation leakage. SecChisel (based on Chisel HDL) gives the ability to design circuitswhich have algorithmically verifiable noninterference property. SecChisel handles thecreation of temporary variables and cascaded propagation of security tags to these newvariables which are unique problems that only occurs when the host language creates anintermediate representation of the designed circuit. SecChisel algorithmically verifies adesign by transforming and modeling the design in a satisfiability modulo theory (SMT)solver. By building and verifying hardware designs, we demonstrate that SecChiselprovides a simple way to verify circuit design's noninterference property at compile timewith no overhead.