Development and formal verification of a new secure provisioning scheme for IoT networks
IoTağları için yeni bir güvenli önyükleme şeması geliştirilmesi ve biçimsel olarak doğrulaması
- Tez No: 865744
- Danışmanlar: PROF. DR. SIDDIKA BERNA ÖRS YALÇIN
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Elektrik ve Elektronik Mühendisliği, Computer Engineering and Computer Science and Control, Electrical and Electronics Engineering
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2024
- Dil: İngilizce
- Üniversite: İstanbul Teknik Üniversitesi
- Enstitü: Lisansüstü Eğitim Enstitüsü
- Ana Bilim Dalı: Elektronik ve Haberleşme Mühendisliği Ana Bilim Dalı
- Bilim Dalı: Elektronik Mühendisliği Bilim Dalı
- Sayfa Sayısı: 126
Özet
Nesnelerin interneti, algılayıcılar ve aktüatörler taşıyan sınırlı donanım kaynaklarına sahip cihazların internet üzerinden veri iletimi sağlamak amacıyla oluşturdukları ağdır. Nesnelerin interneti cihazlarının hayatımızdaki yerinin artmasıyla birlikte, bunların güvenli bir şekilde etkinleştirilmesi, birbirine ve internete bağlanması daha da önemli bir hale gelmektedir. Nesnelerin interneti cihazlarının önyükleme işlemi sırasında oluşabilecek güvenlik açıkları, tüm çalışma yaşamları boyunca taşıyacakları güvenlik zafiyetlerine sebep olabilmektedir. Bu sebeple, nesnelerin interneti cihazlarının bilgi güvenliği parametrelerinin güvenli bir şekilde önyüklenmesi literatürde önemli bir yere sahiptir. Nesnelerin interneti cihazları çok farklı donanım özelliklerine sahiptirler. Bunun yanında, bu cihazlar kullanım amacına göre şekillendirilmiş farklı topolojilere sahip ağlarda yer alabilmektedir. Ayrıca, her uygulama farklı seviyelerde güvenliğe ihtiyaç duyacaktır. Dolayısıyla, nesnelerin interneti cihazlarının güvenli bir şekilde önyükleme yapılması için uygulanabilecek yöntemler, uygulama alanına ve cihazlara özgü zorluklar içermektedir. Nesnelerin interneti cihazların donanım kaynaklarının kısıtlı olması nedeniyle, işlediği verinin ve haberleşmenin güvenliğini sağlayabilecek yazılım gereksinimlerini oluşturmak önemli bir zorluktur. Bilgi güvenliğini sağlamak için kullanılan kriptografik algoritmalar, içerdikleri matematiksel işlemlerin maliyetinden dolayı, önemli miktarda işlemci gücü ve dinamik belleğe ihtiyaç duymaktadır. Bunun yanında, kriptografik işlemlerde anahtar uzunluğuna göre statik bellek ihtiyacı da nesnelerin interneti cihazlarda bir tasarım kısıtı haline gelebilmektedir. Literatürde, nesnelerin interneti cihazlar için önyükleme aşamasını ve haberleşme sırasında ilettiği veriyi güvence altına almak amacıyla sertifika tabanlı birçok uygulama katmanı güvenlik protokolü sunulmuştur. Sertifikaların cihaz içinde saklanması için ihtiyaç duyulan statik bellek gereksinimi ve sertifika tabanlı protokolleri yöneten uygulamaların ve kriptografik algoritmaların çalışabilmesi için gerekli işlemci gücü ve dinamik bellek gereksinimi, kaynak kısıtlı ortamlarda sertifika tabanlı protokoller için önemli bir darboğazdır. Örneğin, Contiki platformları gibi kaynakları kısıtlı nesnelerin interneti cihazları, KB büyüklüğünde statik bellek alanına sahip oldukları için bu tip uygulama seviyesi protokollerle çalışmaya uygun değildir. Bu tezin amacı, yukarıda bahsedilen problemleri göz önünde bulundurarak, yeni bir nesnelerin interneti cihazının güvenli bir şekilde bir internet ağına dahil olma problemini çözmek için yeni bir yöntem önermektir. Bu amaçla, bu tezde nesnelerin interneti cihazlarda bulunan sınırlı kaynaklarla gerçeklenebilecek, literatürdeki benzer çalışmalarla karşılaştırıldığında verimliliği ispatlanabilen ve protokolün bilgi güvenliği literatürde kabul görmüş biçimsel metotlarla doğrulanmış açık anahtar kriptografisine dayalı bir mesaj değişim serisi önerilmiştir. Bu amaçla, tezin ilk aşamasında literatürde var olan önyükleme protokolleri incelenmiş ve bu protokollerin kullanıldığı ortamlar için nasıl özelleştikleri ele alınmıştır. Görülmüştür ki, bazı protokoller üzerinde çalışacağı platformdan bağımsız tasarlanmıştır ve limitli kaynak konusunu bir kısıt olarak göz önünde bulundurmamıştır. Bu sınıfa giren çalışmalar bu tezin hedefi olan nesnelerin interneti için uygun görülmemiştir. Ayrıca bazı protokoller, alana özel çözümler sunarak birçok güvenlik gereksinimini özelleştirmiştir. Bu sınıftaki çalışmalar da bu çalışmanın çözüm aradığı problemin dışında kalmaktadır. Bu literatür taraması da göstermiştir ki nesnelerin interneti için güvenli, kaynak ve performans yönünden verimli bir önyükleme protokolü tasarımı ihtiyaçtır. Bu tezde nesnelerin interneti ortamları için yeni bir anahtar önyükleme ve dağıtım yapısı sunulmuştur. Protokolün tasarımında hedeflenen önemli güvenlik adımları, mesajın güvenliğinin sağlanması, mesaj kaynağının doğrulanması ve mesajın bütünlüğünün korunmasıdır. Tüm bu özelliklerin simetrik anahtar kriptografisi ile elde edilemeyecek olmasından dolayı, tasarım aşamasında asimetrik kriptografiye başvurulmuştur. Burada olası iki seçenek eliptik eğri kriptografisi ve Rivest–Shamir–Adleman (RSA) dir. Daha kısa anahtar uzunluğu ile aynı güvenlik seviyesi sağlaması sebebiyle tasarımda eliptik eğri kriptografisi tercih edilmiştir. Bunun yanında belirtmek gerekir ki; sunulan protokol kriptografik algoritmadan bağımsızdır ve eliptik eğri yerine RSA ile de kullanılabilecek yapıdadır. Eliptik eğrinin daha kısa anahtar uzunluğu ile çalışması, nesnelerin interneti cihazlarının statik bellek kısıtları için de uygun bir seçim olmaktadır. Bir sonraki adımda önerilen yapının güvenlik gereksinimlerini sağladığını doğrulamak için somut matematiksel kanıt sağlamak önemli bir adımdır. Bu amaçla literatür araştırması aşamasında, var olan doğrulama yöntemleri incelenmiştir. Burada biçimsel olmayan ve biçimsel doğrulama yöntemleri ele alınmıştır. Bunlar içerisinden çalışmamızın güvenliğini doğrulayabilecek ve en fazla kapsamayı sağlayabilecek yöntemler seçilmiş ve uygulamak için gerekli altyapı oluşturulmuştur. Önerilen protokolün güvenliğini doğrulamak için ilk olarak biçimsel olmayan analiz metodları uygulanmış ve kullanıcı kişisel gizliliği ve anonimlik saldırısı, tekrarlama saldırısı, ortadaki adam saldırısı ve yerine geçme saldırısı için biçimsel olmayan analiz yapılmıştır. Bir sonraki adım olarak biçimsel metotlara geçilmiş ve ilk olarak BAN mantığı doğrulama süreci uygulanmıştır. Bu süreçte, tüm mesajlar BAN mantığının tanımladığı şekilde idealleştirilmiş, ilk kabullenmeler ve varılmak istenen hedefler tanımlanmış, ardından BAN mantığında yer alan mantıksal kurallar aracılığıyla başta tanımlanan hedeflere varılıp varılamadığı analiz edilmiştir. Önerilen protokol, açık anahtar kriptografisi içerdiği için, genişletilmiş BAN mantığı kural kümesi kullanılmıştır. BAN mantığı analizi sonucunda görülmüştür ki, bu çalışmada önerilen önyükleme protokolü, tanımlanan ilk kabullenmeler ile tanımlanan hedeflere varırken herhangi bir güvenlik açığı oluşturmamaktadır. Literatür araştırması sırasında görülmüştür ki BAN mantığı veri güvenliği açıklarını tespit etmeye yardımcı olabilir ancak bazı uç durumlarda veri güvenliği saldırılarını gözden kaçırabilir. Ayrıca BAN mantığı adımlarında ilk kabullenmeler ve hedefler analizi yapan kişi tarafından tanımlanmaktadır. Burada oluşabilecek bir hatayı ortadan kaldırmak ve çalışma anında bir saldırı varlığında protokoldeki oluşabilecek kusurları da tespit etmek için otomatik bir güvenlik protokolü doğrulama ortamıyla daha doğrulanma süreci yapılmıştır. Bu aşama için AVISPA adı verilen otomatik bir doğrulama ortamı kullanılmıştır. Önerilen protokol, AVISPA ile iki farklı şekilde analiz edilmiştir. İlk olarak sunucu ile geçit arasında oluşturulmuş kanal, çalışmanın kabullenmelerinde de belirtildiği gibi, güvenli kabul edilip sadece önyükleme yapılacak düğüm ile geçit arasındaki mesajlar analiz edilmiştir. Bu yaklaşımla yapılan analiz sonuçları, protokolün güvenli olduğunu doğrulamıştır. İkinci aşama olarak ise protokol uçtan uca tüm mesajları kapsayacak şekilde analiz edilmiştir. Bunun sonucunda da önerilen protokolün veri güvenliği açısından sorunsuz olduğu doğrulanmıştır. Ayrıca, AVISPA nın sağlamış olduğu benzetim ortamı içerisinde farklı senaryolar da test edilmiştir. Saldırı gerçekleştirmek isteyen kişinin geçit veya ana sunucu rollerine bürünmesi durumları da analiz edilmiştir. Bu analiz ile birlikte benzetim ortamında protokolün güvenliği yerine geçme saldırısı yönünden de doğrulanmıştır. Önerilen protokolün güvenliği doğrulandıktan sonraki adım olarak bu protokolün benzer çalışmalar ile karşılaştırılabilmesi için işlem maliyeti hesaplanmıştır. Bu maliyet, kullanılan algoritmalar setine bağlı olduğu için, protokolde eliptik eğri kullanılması durumunda oluşacak maliyet hesaplanmıştır. Literatürde eliptik eğri içeren protokoller incelendiğinde, performans değerleri nokta çarpma işlemi türünden verilmektedir. Var olan çalışmalarla karşılaştırma yapabilmek için bu çalışmada da benzer bir maliyet hesaplama yöntemi uygulanmıştır. Eliptik eğri ile imzalama ve asimetrik şifreleme protokolleri analiz edildiğinde, bir imzalama işlemi için bir eliptik eğri nokta çarpmaya ihtiyaç vardır. Bu imzanın asıllanma maliyeti ise iki nokta çarpma işlemidir. Asimetrik şifreleme için iki nokta çarpma işlemine ihtiyaç varken bu şifrenin çözülmesi bir eliptik eğri nokta çarpma işlemine mal olmaktadır. Son olarak önerilen protokolün gerçeklenebilir olduğunu göstermek ve güç analizi yapabilmek için, tasarlanan protokol nesnelerin interneti için özelleşmiş Contiki işletim sistemi üzerinde gerçeklenmiştir. Bu gerçekleme sonucunda görülmüştür ki önerilen protokol, donanım kısıtları olan bir nesnelerin interneti cihazı için uygulanabilirdir. Bunun yanında, Contiki işletim sisteminin bir parçası olan Cooja benzetim ortamında farklı ağ topolojileri için benzetimler yapılmıştır. Ayrıca, gerçeklenmiş bir protokol için güç tüketim analizi yapmayı sağlayan Cooja benzetim ortamının Powertrace güç analiz ortamında güç tüketimi analizleri yapılmıştır. Yapılan doğrulama çalışmaları ve elde edilen karşılaştırmalar göstermiştir ki önerilen yapı kriptografik işlem sayısı ve kaynak gereksinimleri bakımından literatürde var olan diğer protokollerden daha iyi performansa sahiptir. Ayrıca, bu çalışma farklı donanımlar üzerinde denemelere de açıktır ve bu yönüyle gelecekte farklı donanımların performans karşılaştırmaları için de kullanılabilir bir yapıdadır.
Özet (Çeviri)
IoT is a network of constrained devices carrying sensors and providing data exchange over the internet. With the increase of IoT devices in our life, interconnecting and enabling these devices in a secure manner are becoming essential considerations. Due to the resource-constrained nature of IoT devices, meeting the requirements of a secure infrastructure also becomes a challenge. To date various certificate-based application layer exchange protocols have been introduced to secure network traffic. The bottleneck of certificate-based protocols in resource constrained environments is storage size since certificates and applications to manage certificate-based protocols require additional storage and dynamic memory. The resource constrained IoT devices such as Contiki platforms suffer with these protocols since they have KB magnitude flash area. Enabling a new IoT node into a live network securely is also suffering from these challenges. The aim of this thesis is to propose a lightweight, elliptic curve-based message exchange series to solve secure provisioning of IoT devices. For this purpose, we present a novel ECC based key distribution scheme for IoT environments. Moreover, it is an essential step to provide concrete mathematical proof to verify if the proposed scheme meets the secure requirements. For this purpose, we apply BAN logic formal verification process to prove that our scheme is formally verified and secure. Beside that, The BAN logic can help to spot weaknesses but based on the literature it may miss attacks in some edge cases. For the sake of filling the gap, we tested our security protocol with an automated verification environment called AVISPA. The aim is to detect any flaws in the protocol design by considering the execution in the presence of an adversary. Our comparison show that our implementation has better performance than other listed protocols with its number of cryptographic operations and resource requirements.
Benzer Tezler
- Model driven security framework for software design and verification
Yazılım tasarımı ve doğrulama sürecinde model güdümlü güvenlik çerçevesi
ENGİN DEVECİ
Doktora
İngilizce
2015
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBoğaziçi ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. MEHMET UFUK ÇAĞLAYAN
- İnternette heterojen veri kaynaklarından verinin toplanması, doğrulanması ve sorgulanması
Collecting, verifying, and inquiring data from heterogeneous data sources on the internet
SERDAR KÜRŞAT SARIKOZ
Doktora
Türkçe
2023
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolGazi ÜniversitesiBilgisayar Bilimleri Ana Bilim Dalı
PROF. DR. MUHAMMET ALİ AKCAYOL
- Kalite güvence sistemindeki bazı öğelerin denetim sürecine ilişkin bilgi tabanlı bir uzman sistem yaklaşımı
Başlık çevirisi yok
DEMET BAYRAKTAR
- Bir maliyet + kar projede 'şube yenileme işleri' malzemenin temini ve lojistik
Başlık çevirisi yok
HASAN GÜNEY DEMİR
Yüksek Lisans
Türkçe
1998
İnşaat Mühendisliğiİstanbul Teknik ÜniversitesiYapı İşletmesi Ana Bilim Dalı
PROF. DR. DOĞAN SORGUÇ
- Architecture of constraints: A mass customization oriented approach for housing design
Kısıtlarla tanımlanan mimarlık: Kitlesel özelleştirme odaklı konut tasarımı
BENGİSU İLKSOY
Yüksek Lisans
İngilizce
2015
Mimarlıkİstanbul Teknik ÜniversitesiMimarlık Ana Bilim Dalı
DOÇ. DR. MİNE ÖZKAR KABAKÇIOĞLU