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ı: 70
Ö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
- Düşey kanallarda farklı kanat düzenlemelerinde doğal taşınımla ısı geçişinin sayısal olarak incelenmesi
Numerical investigation of natural convection heat transfer in vertical channels with different fin arrangements
KAAN KISA
Yüksek Lisans
Türkçe
2024
Makine Mühendisliğiİstanbul Teknik ÜniversitesiMakine Mühendisliği Ana Bilim Dalı
DR. ÖĞR. ÜYESİ TURGUT YILMAZ
- Schedulability analysis of real-time multi-frame co-simulations on multi-core platforms
Çok-çekirdekli platformlarda gerçek zamanlı çok-çerçeveli eş-benzetim için çizelgelenebilirlik çözümlemesi
MUHAMMAD UZAİR AHSAN
Doktora
İngilizce
2020
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolOrta Doğu Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET HALİT SEYFULLAH OĞUZTÜZÜN
- Automatic Selection of Statistical Model Checkers for Analysis of Biological Models
Başlık çevirisi yok
MEHMET EMİN BAKIR
Doktora
İngilizce
2017
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolThe University of SheffieldPROF. DR. DANIŞMAN YOK
- Formal specification of fragmentation and reassembly in IPv6
Başlık çevirisi yok
İBRAHİM ŞAHİN
Yüksek Lisans
İngilizce
1997
Elektrik ve Elektronik MühendisliğiOld Dominion UniversityDR. JAMES F. LEATHRUM, JR.
- Sigorta şirketlerinde denetim
Inspection at insurance companies
YASEMİN GÜL
Yüksek Lisans
Türkçe
2001
SigortacılıkMarmara ÜniversitesiSigortacılık Ana Bilim Dalı
PROF.DR. ŞAHAMET BÜLBÜL