A tool for verifying noninterference property for HDL
Donanım tasarlama dilinin birbirine karışmamışlık özelliğini doğrulayan araç
- Tez No: 472600
- Danışmanlar: YRD. DOÇ. DR. ONUR DEMİR
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Computer Engineering and Computer Science and Control
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2017
- Dil: İngilizce
- Üniversite: Yeditepe Üniversitesi
- Enstitü: Fen Bilimleri Enstitüsü
- Ana Bilim Dalı: Bilgisayar Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: Belirtilmemiş.
Özet
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
Özet (Çeviri)
Hardware description languages started to adopt high-level functionalities. Through the flexibility of high-level programming, hardware designers can leverage object-oriented programming and functional programming paradigms to specify the hardware for quicker design time. This transition to high-level hardware descriptions created a new set of problems 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 preventing information leakage. SecChisel (based on Chisel HDL) gives the ability to design circuits which have algorithmically verifiable noninterference property. SecChisel handles the creation of temporary variables and cascaded propagation of security tags to these new variables which are unique problems that only occurs when the host language creates an intermediate representation of the designed circuit. SecChisel algorithmically verifies a design by transforming and modeling the design in a satisfiability modulo theory (SMT) solver. By building and verifying hardware designs, we demonstrate that SecChisel provides a simple way to verify circuit design's noninterference property at compile time with no overhead.
Benzer Tezler
- Tasarımda yangın güvenliği açısından kaçış mesafelerinin denetiminde YBM tabanlı karar destek modeli
A BIM-based decision support model for verifying escape distances in terms of fire safety in design
ÇİĞDEM FIRAT
- Development of postprocessor, simulation and verification software for a five-axis CNC milling machine
Beş-eksen CNC freze tezgahı için son-işlemci, simülasyon ve doğrulama yazılımı geliştirilmesi
ENDER CENGİZ
Yüksek Lisans
İngilizce
2005
Makine MühendisliğiOrta Doğu Teknik ÜniversitesiMakine Mühendisliği Bölümü
PROF.DR. MUSTAFA İLHAN GÖKLER
- Development of a coverage-driven cocotb-based functional verification framework for the RISC-V load-store and r-type instructions
Rısc-v yükleme-saklama ve r-tipi buyrukları için kapsam odaklı cocotb tabanlı bir fonksiyonel doğrulama ortamının geliştirilmesi
ŞENNUR GÜNEY
Yüksek Lisans
İngilizce
2024
Elektrik ve Elektronik MühendisliğiGebze Teknik ÜniversitesiElektronik Mühendisliği Ana Bilim Dalı
DR. ÖĞR. ÜYESİ İHSAN ÇİÇEK
- Ankara örnekleminde 12-36 aylık bebek ve çocuklar için sosyal ve duygusal değerlendirme aracının türk çocuklarına uyarlanması
Adapting social and emotional assesment tool for 12-36 months old babies and children to Turkish children
YASEMİN ALPAN
Yüksek Lisans
Türkçe
2006
Eğitim ve ÖğretimGazi ÜniversitesiÇocuk Gelişimi ve Eğitimi Ana Bilim Dalı
YRD. DOÇ. DR. ADALET KANDIR
- Kesici ağzı yuvarlatılmış takım ile ortogonal talaş kaldırma için geliştirilen kayma hattı modeline dayalı yeni takım- talaş temas uzunluğu bağıntısı
New tool-chip contact length relationship based on the developed slip-line model for orthogonal cutting with rounded cutting edge tool
ŞÜKRÜ KOCABAŞ
Doktora
Türkçe
2024
Makine MühendisliğiYıldız Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
PROF. DR. ERHAN ALTAN