Web uygulamalarının kullanımı artık tüm alanlar için kaçınılmaz bir hale gelmektedir; ticaret, eğitim, sağlık, devlet gibi birçok alandaki hizmetler web uygulamaları aracılığıyla iletilmekte ve web teknolojilerinin hızla gelişmesiyle bu uygulamaların kullanımı giderek artmaktadır [22]. Web uygulamalarında var olan hataların tespiti için etkili bir yöntem ihtiyacı ise giderek önem kazanmaktadır. Yetersiz dolaşım özellikleri web uygulamalarındaki en yaygın hatalardan birini oluşturmaktadır. Gidecek bir sonraki sayfası olmayan, çıkmaz sayfalar (dead end) ve ulaşılamayan web sayfaları kullanılabilirliği azaltan dolaşım hatalardan bazılarıdır. De Alfaro [9] ve Di Sciascio v.d. [12] çıkmaz sayfaların bulunmamasının iyi tasarımın gereksinimlerinden biri olduğunu belirtmişlerdir. Ayrıca, web uygulamalarında kullanıcılardan yetki bilgisini isteyen servislerin erişim kontrolündeki eksiklikler önemli bir başka hata kategorisini oluşturmaktadır. OWASP 2013 web uygulamaları güvenlik açıkları ilk 10 listesinde [23] 7. sırada yer alan "Eksik işlev seviyesindeki erişim kontrolü" ve CWE 2011 en tehlikeli 25 yazılım hataları listesinde [7] 6. sırada yer alan "Eksik yetkilendirme" maddeleri bu tip erişim hatalarını kapsamaktadır. Bu ve benzeri erişim kontrolü hatalarını ve dolaşım hatalarını önlemek veya tespit etmek için model denetleme kullanılan metotlardan biridir ( [9], [11], [14], [15], [16]).
Formel sistem modellerinin, verilen zamansal mantık özellikleriyle otomatik doğrulanması için geliştirilen model denetleme metodu, web doğrulanması için kullanılması avantajlı bir metottur; model denetleme otomatik olarak, kullanıcı desteğine ihtiyaç duymadan, sistem modelinin uzayında kapsamlı arama ve denetleme yapabilmektedir. Ayrıca, model denetleme ihlal edilen her özellik için ürettiği karşı örneklerle hatanın bulunmasını kolaylaştırmaktadır. Fakat, bu getirilerine rağmen, model denetleme, formel metotlar ile ilgili deneyimsiz geliştiriciler için uygulaması zor bir metottur. Ek olarak, web uygulamasının formel modelinin çıkarılması, model denetleme uygulanmasını zorlaştıran başka bir nedendir. Çünkü karmaşık yapılarıyla, web uygulamaları, modellenmesi zor sistemlerdir. Tüm bu nedenler, model denetlemenin web uygulamalarının doğrulanması için tercih edilmemesine neden olmaktadır.
Bu çalışmada, model denetleme tekniğini deneyimsiz kullanıcılara arka plandaki formel metotlar olmaksızın uygulatmak, dolaşım ve erişim kontrolü hatalarının sembolik model denetleme ile tespit edilmesi amaçlanmıştır. Geliştirilen araç, web uygulamasının Crawljax [21] ve WebMole'un [19] bir başka versiyonu olan, Micro-Crawler araçlarıyla elde edilmiş statik gösterimini model olarak kabul etmektedir. Model denetleme aracı olarak ise NuSMV [6], bir sembolik model denetleme aracı kullanılmaktadır. Sunulan yöntem web crawler araçlarının çıktısının web modele çevrilmesi, sembolik model denetleme ve karşı örneklerin canlandırılması için otomatik çalıştırılabilir betik üretme işlemlerini birleştirmektedir.
Model denetleme ile web uygulamalarının doğrulaması birçok kez denenmiş bir yöntemdir. Model denetleme araçları, web tasarımı doğrulaması, desteklenmesi ( [5], [12], [14], [22]), hata tespiti [1] ve web akışını kontrol etmede [15] kullanılabilmektedir. Web uygulamalarının formel modellerini oluşturmak, amaçlar farklı olsa da, model denetlemeyi kullanan tüm çalışmalarda ortak bir süreçtir. Modelleme, model denetleme yönteminde kilit bir öneme sahiptir, çünkü model bazlı herhangi bir doğrulama işlemi sadece sistemin modeli kadar iyidir [2]. Web uygulamaları genelde dinamik betiklerle yazıldığı ve kullanıcı etkileşimleri uygulamanın akışını dinamik olarak oluşturduğu için, statik analizle yapılmış modelleme dolaşımsal hataların bulunmasındaki potansiyeli sınırlamaktadır [1]. Buna rağmen statik analiz ile, kaynak koddan, elde edilen model web uygulamalarının kontrol akışını doğrulamakta kullanılabilmektedir [20]. Dinamik analizle modellemeye bir örnek olan Haydar v.d.'nin çalışmasında harici davranışları izlenerek, http istek/cevapları, web uygulamasının modeli yaratılmaktadır [17]. Bazı çalışmalarda ise web uygulaması modeli manuel olarak özel bir modelleme diliyle tanımlanmakta, ardından bu model, model denetleme aracının diline çevrilmektedir ( [15], [24]). Ayrıca, var olan bir web uygulamasının modelini web crawler yardımıyla çıkarmak da mümkündür. Fakat, bu çok doğrudan bir süreç değildir [10], çünkü artan etkileşim ve dinamik içerikten dolayı web uygulamalarının bu şekilde modellenmesi zor bir süreç haline gelmektedir. Bu çalışmada, bahsedilen sebepten dolayı AJAX tabanlı web uygulamalarını crawl edebilme kabiliyetine sahip araçlar kullanılmaktadır.
Otomatik web doğrulama araçlarından AnWeb [12], web uygulamalarının tasarımlarını desteklemek için geliştirilmiştir. AnWeb'de model, kullanıcı form doldurma işlemleri için sunucu ve statik sayfaları belirlemek için istemci kodlarından oluşturulmaktadır. Model durumlarını web sayfaları, pencereler ve linkler oluşturmaktadır. WaVer [5] ise web uygulamalarının tasarımını denetlemek amacıyla UML diyagramlarını doğrulayan bir araçtır. NuSMV model denetleme aracının kullanıldığı bu çalışmada, çıktılar UML diyagramında gerekli düzenlemelerin yapılması için kullanılmaktadır. AnWeb ve WaVer'de formel modelleme otomatikleştirilmekte, model denetleme ise yazarlar tarafından hazırlanan özelliklerle uygulanmaktadır. Miao ve Zeng ise özelliklerin üretimini verilen tasarım diyagramı yardımıyla otomatikleştirmektedir [22]. Denetlenecek model ise web uygulamasının implementasyon modelini temsil etmekte ve manuel olarak tanımlanmaktadır. [22]'de tasarım modeli, özellikler için bir taban oluştursa da kullanıcı özellik tanımlama işleminin dışında kalmıştır. Denetlenecek özelliklerin kullanıcı tarafından tanımlandığı çalışmalar da mevcuttur ( [4], [11], [17]). Bu yolla, deneyimsiz kullanıcılar için model denetleme aracının uygulaması daha anlaşılabilirleştirilse de, bu uygulamanın çıktısının anlaşılması için bir çeviri işlemi yapılmadığı gözlenmektedir. Hata çıktısının anlaşılabilirliğini gözeten bir çalışmaya örnek VeriWeb'dir [3]. VeriWeb, interaktif web uygulamalarındaki tüm yürütme yollarını keşfetmek ve analiz etmek için geliştirilen bir araçtır. Bu çalışmada VeriSoft'u kullanarak belirlenemezci bir algoritmayla arama ve keşfetme işlemi gerçekleştirilmekte, ayrı bir bileşenle yürütme yollarındaki hatalar tespit edilmekte ve WebVCR adlı kaydet/oynat aracıyla canlandırılabilmektedir. Fakat hata oynatma, otomatik olarak yapılmamakta bunun yerine kullanıcıya bir seçenek olarak sunulmaktadır.
Geliştirilen aracın ayrıntılı çalışma akış şeması Şekil
Şekil 2'de örnek bir ara web modeli gösterilmektedir. İlk satır webstate tanımını ifade etmektedir. Bu formatta, bağlantı ilişkisi <edge> ve </edge> etiketleri arasında verilmiştir ve her biri, w i , <from> etiketiyle tanımlanan bir webstate, w j , <to> etiketiyle tanımlanan webstate ve w i ve w j arasındaki geçişleri tetiklemek için tıklanan elementin XPath ifadesini içeren etiketlerinden oluşturulmuştur. Şimdilik, geçiş sadece tıklama olayıyla tanımlanmıştır, geri tuşu ise dikkate alınmamıştır. Bu kısıtlamanın sebebi ise web crawler tarafından üretilen sonlu sistem modellerinden kaynaklanmaktadır.
Web crawler modelinin ara web modele çevrilmesinin ardından kullanıcılar eksik olduğunu düşündükleri webstate veya geçiş tanımlarını aracın arayüzü yardımıyla ekleyebilmektedir. Ayrıca, kullanıcı kendi web modelini elle tanımlayabilmektedir.
Web crawler aracından alınan web modelin ara web modeline dönüştürülmesinin ardından (Şekil 2) NuSMV modeli yaratılır. Aracımız, denetlenecek özellikleri CTL (Hesaplama Ağacı Mantığı, Computation Tree Logic) formülleri şeklinde tanımlar. CTL özellikleri hakkında detaylı açıklama bölüm 3.3'te, NuSMV modelinin yaratılması ise bölüm 3.2'de verilmektedir. En son aktivite olan karşı örneklerin Selenium Webdriver kütüphaneleri ile web tarayıcı üzerinde yürütülen çalıştırılabilir senaryolara çevrilmesidir. Bu işlem ise bölüm 3.4'te açıklanmaktadır.
Bu bölümün geri kalanında, aracın ara web modelinin oluşturulmasının ardından çalışma işleyişi örnek bir uygulama (Şekil 3) üzerinden anlatılmaktadır. Örnek web uygulaması 6'sı php dosyası olmak üzere 12 kaynak dosyasından oluşmaktadır. Uygulama özellikle geliştirilen araçla bulunabilen hataların gösterimi için tasarlanmıştır. Örnek uygulamada, AJAX tabanlı bir sayfa, bir oturum açma sayfası ve oturum açma gerektiren bir kaç sayfa, 2 çıkmaz sayfa ve 1 geçersiz bağlantı bulunmaktadır. Bu ASSIGN bölümünde öncelikle değişkenlerin ilk değerleri init yapısı ile atanmıştır (satır 8-10). Element değişkenine, henüz hiçbir elemente tıklanmadığını belirtmek için, null_element değerini atanmıştır. Webstate değişkeninin ilk değeri uygulamanın açılış sayfası olan index'tir. Koruma koşulu değişkeni login, false değerini almıştır.
İlk değerlerin tanımlanmasının ardından, her bir değişkenin bir sonraki adımda alacağı değeri case yapısı içinde geçiş ilişkileri ile tanımlanmaktadır. Case yapısında her bir kısım bir koşul, noktalı virgül ve değişkenin alacağı değerden oluşmaktadır. TRUE kelimesiyle başlayan son case koşulu diğer hiçbir koşulu sağlamayan değişken değerlerinin aldığı değeri, (default value) belirtmektedir.
Şekil 4'te 11 ve 27. satırlar arasında tanımlanan webstate değerinin geçiş ilişkileri <edge>,</edge> etiketleri içinde tanımlanan bilgilere göre tanımlanmaktadır. Ara web model anlatımında değinildiği gibi geçişler <from>, <to> ve <XpathOfElement> alt öğelerinden oluşmaktadır. Webstate case koşulları <from> etiketi ve değiştirilmiş XPath ifadesiyle eşleşen elemanın tıklanma olayından oluşmaktadır. Buradaki next ifadesi eleman değişkeninin bir sonraki adımdaki değerini gösterir. Eleman değeri modeldeki bir webstate değerinden ötekine geçmek için gerekli olan tıklanabilir eleman bilgisini vermektedir. Bu yüzden, eleman değişkeni bir önceki webstate içindeki son tıklanan elemanı vermektedir. Son olarak, hiç bir geçiş sağlanamadığında tuzak durum olarak dead_end_webstate geçişini tanımlanmaktadır (Satır 26).
Eleman değişkeninin bir sonraki değeri o anki webstate değerinin, DOM ağacındaki tıklanabilir elemanlar arasından rastgele seçilmektedir (Satır 28-36). Eğer webstate dead_end_webstate değerini almışsa, sistemin tuzak durumunda kalmasını sağlamak için eleman değeri null_element olarak sabitlenmektedir (satır 36).
Örnek web uygulamasında bir oturum açma koşulu bulunmaktadır. Bu koşul modele kullanıcının aracımız yardımıyla oturum açma ve kapama geçiş ilişkilerini tanımlamasıyla eklenmiştir. Oturum açma Şekil 5 satır 40 ile verilmektedir. Bu bilgi ayrıca satır 13'ü de etkilemektedir. Satır 13 ile başarılı bir oturum açma işlemiyle state2'ye ulaşılabileceği bilgisi eklenmektedir. Oturum kapama ise satır 41'de tanımlanmaktadır. Örnek web uygulamasının modelinin, belirtilen CTL formülleri ile model denetleme aracıyla yürütülmesi 7 karşı örneğin oluşmasına neden olmuştur. Index ulaşılabilirliği, state9, state4 ve state14 tarafından, çıkmaz sayfa yokluğu aynı webstate'ler tarafından ihlal edilmiştir. Erişim kontrolü özelliği ile ise aslında özel bir durum olması gereken state4'ün oturum açılmadan erişilebildiği tespit edilememiştir.
NuSMV karşı örneklerinden JUnit kodu üretimi, hazırlanan şablon dosyadan yararlanılarak yapılmaktadır. Şablon dosyada Selenium ve JUnit paketlerinin içeri aktarım satırları, setup ve teardown metotlarının ortak kodları bulunmaktadır. Setup metodunda tarayıcı ilk kullanıma hazırlanmakta, teardown adlı metotta ise karşı örneği açıklayan diyalog kutusu gösterilmektedir. Karşı örneklerdeki ihlale neden olan adımlar test metodunun içine, şablona sonradan eklenerek tanımlanmaktadır.
Şekil 6, NuSMV tarafından AG(webstate=state4->EF(webstate=index)) özelliğinin modelde ihlal edilmesiyle üretilen karşı örnek vermektedir. Şekil 7, bu karşı örnek ile üretilen JUnit kodunu vermektedir. Ayrıca özellik bilgisi note değişkeniyle teardown metoduna diyalog kutusunu yaratmak için kullanılmıştır. Şekil 6'da hataya neden olan adımlar görülmektedir. Buna göre state4 index sayfasına ulaşamadığı için, state4'e giden yürütme adımları karşı örneği oluşturmaktadır. Bu yüzden Şekil 7'deki test metodunun içinde, index'ten state4'e giden adımlar bulunmaktadır. Test metodu web uygulamasının URL adresinin belirtilmesiyle başlamakta ve hataya yol açan durumlara karşı örnekte yer alan XPath ifadeleriyle eşleşen tıklanabilir elemanlara tıklanmasıyla devam etmektedir. Karşı örnekte NuSMV koduna uyum sağlaması için değiştirilen XPath ifadesi, JUnit koduna çevrilirken orijinal haline dönüştürülmektir.
Geliştirilen aracın değerlendirilmesi 3 adımda gerçekleştirilmiştir. İlk olarak aracın kullanılabilirliğini ölçmek için bir anket uygulanmıştır. Ardından, 14 gerçek uygulama üzerinde aracın dolaşım hata tespit etme kapasitesi değerlendirilmiştir. Son olarak erişim kontrolü hatası bulma kapasitesini ölçmek için hata enjeksiyonu kullanılmıştır. Deneyler, Intel Core i5-3210 Windows 7 ve 4GB RAM bilgisayarda sürdürülmüştür.
Kullanılabilirlik çalışmasının uygulandığı grup ODTÜ Enformatik Enstitüsü web admini, Drupal ile ileri derece web geliştirme deneyimi olan bir doktora öğrencisi, ikisi web geliştirme deneyimi olan, biri php-Mysql deneyimi olan yüksek lisans öğrencileri ve web geliştirme deneyimi olmayan 1 yüksek lisans ve 1 lisans öğrencisi tarafından oluşturulmuştur. Katılımcıların hiçbirinin formel tekniklerle ilgili bilgisi bulunmamaktadır. Aracın, yaklaşık 10 dakika kullanıcılara tanıtılması ve nasıl kullanılacağının anlatılmasının ardından, doğrulama işleminin yapılması istenmiştir. İşlem web crawlerdan çıkan modelin araca yüklenmesi, otomatik olarak üretilen özelliklerle doğulama yapılması, bir bağlantı tutarlılığı özelliği eklenmesi ve bulunan hataların tarayıcı üzerinde oynatılmasından oluşmaktadır.
Hiçbir formel metot deneyimi olmayan kullanıcılar araç sayesinde CTL özelliği eklemeyi ve web uygulamasını model denetleme kullanarak doğrulamayı başarmışlardır. Bu deneyimin ardından katılımcılara 5 soruluk, likert ölçümüne göre hazırlanmış kullanılabilirlik anketinin tamamlanması istenmiştir. Anket, teknoloji kabul modeli (TAM) [8] faktörleri olan, algılanan kullanım kolaylığı ve algılanan yararlılık, gözetilerek hazırlanan 5 sorudan oluşturulmuştur. Sonuçlar (bkz. Ek, Tablo A-2) hata canlandırılmasının yararlı bir işlev olacağını öngörmektedir. Kullanım kolaylığı faktörünün düşük sonuçları ise geliştirilen aracın ticari bir yazılım olmadığı için kabul edilebilirdir.
Ulaşılabilirlik hatalarının tespiti performansının değerlendirilmesi için 14 web uygulaması kullanılmıştır (bkz. Ek, Tablo A-1). Bu uygulamalar php, asp.net ve java gibi farklı programlama dilleri ile geliştirilmiş, Apache veya IIS 6.0 web sunucularında çalışmaktadırlar. Kullanılan web teknolojileri arasında AJAX da bulunmaktadır.
Web uygulamaların modelleri Micro-Crawler aracıyla çıkarıldı. Aracın modeli doğrulaması ardından, toplamda 70 karşı örnek üretilmiştir. Her bir web uygulaması için tüm işlem minimum 203 ms (milisaniye), maksimum 2384 ms sürdü. Süre analizine göre medyan 864 ms, ortalama süre ise 533 ms varyansla 961 ms olmuştur. Karşı örneklerden 26 tanesi gerçek uygulamada hata olmayan yanlış gösterimler olmuştur. Yanlış alarm adını verdiğimiz bu karşı örneklerin web crawler aracının modelinin yetersizliğinden ortaya çıktığı gözlemlenmiştir. Örneğin W7 uygulamasında web crawler index ve bir durum arasındaki bağlantıyı rapor etmemiş, bu da iki tane yanlış karşı örneğe neden olmuştur. Bu durumu incelemek için, 3 tane web uygulaması (W7, W12 ve W14) seçilmiş ve model, tarayıcı üzerinden gösterilen hata senaryoları incelenerek, geliştirilen aracın arayüzüyle modeller rafine edilmiştir.
Erişim kontrolü hatalarının bulunmasının performansını değerlendirmek için, açık kaynaklı ve php ile geliştirilen Restaurant Script1 adlı web uygulamasına hata enjekte edilmiştir. Bu uygulamada kullanıcılar web sitesine kayıt olup, kartları yardımıyla pizza siparişi verebilmektedir. Uygulama kaynak dosyalarından, "auth.php" oturum açma alanlarında doldurulan bilgilerin doğruluğunu kontrol etmektedir. Deney kapsamında, bu dosyanın diğer dosyalara eklendiği satırlar yorum haline getirilerek yetki kontrolünün bazı işlemler için yok sayılması sağlanmıştır. (Şekil 8). Bu yolla web uygulamasının 3 hatalı versiyonu yaratılmıştır. Bir versiyonda sadece üyelik işlemleriyle ilgili dosyalara hata enjekte edilmiştir. Diğer versiyonda kart işlemlerinin yetki alanları değiştirilmiştir. Son olarak hem kart hem de üyelik işlemlerine hata enjekte edilmiştir. Versiyon 1,2 ve 3'te bulunan karşı örnekler yalnızca enjekte edilen hatanın bulunduğu dosyayla ilgilidir. Erişim kontrolü hataları, araç yardımıyla tespit edilebilmiştir.
Bu çalışmada, formel metot bilgisi olmayan kullanıcılara, model denetleme ile web uygulamalarını doğrulama imkanı vermek için bir yaklaşım ve araç geliştirilmiş, bu kapsamda, modelleme işlemi, zamansal özelliklerin tanımlanması ve üretilen karşı örneklerin anlamlandırılması sağlanmıştır. Ayrıca web crawler'ların ürettiği web model formatları model denetlemede kullanılmış, kullanıcının sıfırdan bir model geliştirmesine gerek kalmamıştır. Geliştirilen aracın kullanılabilirliği formel metot bilgisi olmayan fakat web geliştirmeyle ilgili farklı seviyelerde bilgisi bulunan katılımcılarla değerlendirilmiş ve aracın hata bulma, görselleştirmesinde yararlı olduğu, ama kullanım kolaylığı açısından zayıf kaldığı gözlemlenmiştir. Hata tespit etme performansı ise ulaşılabilirlik ve erişim kontrolü için ayrı değerlendirilmiş, sonuçlara göre, 14 uygulamada 44 ulaşılabilirlik hatası ve 1 web uygulamasına kusur enjekte edilerek tüm erişim kontrolü hataları araç yardımıyla tespit edilmiştir.