Arduino için Donanım Modeli PLC Doğrulamasındaki Yanlış Alarmları Gideriyor
Arduino tabanlı endüstriyel kontrol sistemlerinde IEC 61131-3 PLC kodu için donanım farkındalıklı doğrulama, yanlış alarmları ortadan kaldırıyor.
IEC 61131-3 PLC programları için kullanılan açık kaynaklı doğrulayıcılar (ESBMC-PLC gibi), gerçek donanımdan bağımsız, sınırsız tam sayılarla çalışan soyut bir tarama döngüsü modeli üzerinden güvenlik kanıtlar. Ancak OpenPLC, Arduino OPTA, CONTROLLINO ve Industrial Shields M-Duino gibi düşük maliyetli endüstriyel kontrolörler 16-bit kelimelerle çalışan mikrodenetleyicilerde ve sonlu çözünürlüklü ADC'lerle çalışır; bu da doğrulama modeli ile gerçek dağıtım arasında bir uçurum yaratır.
Araştırmacılar 123 gerçek programı analiz ettiğinde, donanım modeli olmadan yapılan 16-bit taşma kontrolünün %44 oranında yanlış alarm ürettiğini (123 programın 54'ünde) ve hiçbir gerçek kusur bulamadığını gösterdi; çünkü bu yaklaşım hiçbir ADC'nin üretemeyeceği sensör değerlerini araştırıyordu. Bu durum kritiktir çünkü taşma, yüksek seviye alarm gibi bir güvenlik eylemini sessizce bastırabilir, sınırsız girdi modelleri ise hiçbir ortamın tetikleyemeyeceği sahte alarmlar üretebilir.
Bu çalışma, genişlik, ADC/PWM çözünürlüğü ve I/O bağlantısını tanımlayan bildirimsel bir donanım soyutlama katmanı (HAL) tanımlayıcısı ve girdileri donanımla gerçekleştirilebilir aralıklarla sınırlayan sağlam bir indirgeme sunuyor. Arduino için ArduinoTool olarak somutlaştırılan bu yaklaşım, ESBMC'nin Ladder Diagram ön ucuna entegre edildi.
123 programlık test setinde HAL açıklayıcısı, sağlamlık kanıtlarını korurken 54 yanlış alarmın tamamını ortadan kaldırdı; kontrollü bir test setinde ise gerçekleştirilebilir tanıklarla nadir görülen genişliğe bağlı kusurları tespit etti. Bu sonuç, ICS güvenliği araştırmalarında kullanılan düşük maliyetli otomasyon donanımları için biçimsel doğrulamanın pratikte güvenilir hale gelmesi açısından önemli.