Automata-based model counting string constraint solver for vulnerability analysis
Başlık çevirisi mevcut değil.
- Tez No: 626160
- Danışmanlar: PROF. TEVFİK BULTAN
- Tez Türü: Doktora
- 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: University of California Santa Barbara
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 131
Özet
Most common vulnerabilities in modern software applications are due to errors in string manipulation code. String constraint solvers are essential components of program analysis techniques for detecting and repairing vulnerabilities that are due to string manipulation errors. In this dissertation, we present an automata-based string constraint solver for vulnerability analysis of string manipulating programs. Given a string constraint, we generate an automaton that accepts all solutions that satisfy the constraint. Our string constraint solver can also map linear arithmetic constraints to automata in order to handle constraints on string lengths. By integrating our string constraint solver to a symbolic execution tool, we can check for string manipulation errors in programs. Recently, quantitative and probabilistic program analyses techniques have been proposed which require counting the number of solutions to string constraints. We extend our string constraint solver with model counting capability based on the observation that, using an automata-based constraint representation, model counting reduces to path counting, which can be solved precisely. Our approach is parameterized in the sense that, we do not assume a finite domain size during automata construction, resulting in a potentially infinite set of solutions, and our model counting approach works for arbitrarily large bounds. We have implemented our approach in a tool called ABC (Automata-Based model Counter) using a constraint language that is compatible with the SMTLIB language specification used by satisfiability-modulo-theories solvers. This SMTLIB interface favii cilitates integration of our constraint solver with existing symbolic execution tools. We demonstrate the effectiveness of ABC on a large set of string constraints extracted from real-world web applications. We also present automata-based testing techniques for string manipulating programs. A vulnerability signature is a characterization of all user inputs that can be used to exploit a vulnerability. Automata-based static string analysis techniques allow automated computation of vulnerability signatures represented as automata. Given a vulnerability signature represented as an automaton, we present algorithms for test case generation based on state, transition, and path coverage. These automatically generated test cases can be used to test applications that are not analyzable statically, and to discover attack strings that demonstrate how the vulnerabilities can be exploited. We experimentally compare different coverage criteria and demonstrate the effectiveness of our test generation approach.
Özet (Çeviri)
Özet çevirisi mevcut değil.
Benzer Tezler
- Modelling of Population Dynamics in Cell Cultures
Hücre Kültürlerindeki Nüfus Dinamiğinin Modellenmesi
ÇİĞDEM AKSU
Yüksek Lisans
İngilizce
2010
BiyolojiBoğaziçi ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
DOÇ. DR. YAĞMUR DENİZHAN
- Ayrık olay sistemlerinin tasarımı ve kontrolü için yeni bir gerçekleme ve otomatik kod üretme yöntemi
A new realization and automatic code generation method for the design and control of discrete event systems
İBRAHİM TOLGA HASDEMİR
Doktora
Türkçe
2009
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiElektrik Mühendisliği Ana Bilim Dalı
DOÇ. DR. SALMAN KURTULAN
- İstanbul'da kentsel büyümenin senaryo tabanlı modellenmesi ve ekolojik açıdan değerlendirilmesi
Scenario-based modeling and evaluation of urban growth in Istanbul
ALİYE GONCA BOZKAYA KARİP
Doktora
Türkçe
2024
Şehircilik ve Bölge PlanlamaMimar Sinan Güzel Sanatlar ÜniversitesiŞehir ve Bölge Planlama Ana Bilim Dalı
PROF. DR. FATMA ÜNSAL
- Hücresel özdevinim ve yapay sinir ağları yaklaşımı ile coğrafi bilgi sistemi verilerine dayalı kent benzetim modeli: izmir örneği
Urban simulation model based on geographic information system data using cellular automata and artificial neural networks approach: the case of izmir
NUR SİPAHİOĞLU
Yüksek Lisans
Türkçe
2020
Mimarlıkİstanbul Teknik ÜniversitesiBilişim Ana Bilim Dalı
PROF. DR. GÜLEN ÇAĞDAŞ
- Hücresel otomat tabanlı sleuth model kullanılarak kentsel büyümenin tarım alanları üzerindeki etkisinin incelenmesi
Investigation of the effect of urban growth on agricultural lands using cellular automata based sleuth model
MURAT GÜNEŞ
Yüksek Lisans
Türkçe
2023
Jeodezi ve FotogrametriKonya Teknik ÜniversitesiHarita Mühendisliği Ana Bilim Dalı
DR. ÖĞR. ÜYESİ LÜTFİYE KARASAKA