Software Verification

A program is a mathematical object. A programming language is a mathematical language. Therefore, proving properties of a program should be possible. Does the program do what is supposed to do? Does it not do anything harmful? Is it possible to answer these questions?

In spite of the fact of being a mathematical object for a program, the answer is probably no if we think about all. A programming language is also a formal language. By the definition, the set of inputs upon which a certain Turing Machine halts. This definition denotes that each well formed program would compile or not. The compiler itself is a program too. According to this induction, perhaps it seems possible to prove properties of every program. But it is not.

Turing machine halting problem is NP-complete. In complexity theory, the NP-complete problems are the most difficult problems in NP (nondeterministic in polynomial time). It is not possible to decide when the program terminates this is why the Turing machine halting problem is NP-complete. It is possible to prove sequential programs. You do only some checks on the actions the program do. But loops used inside a program makes deciding very hard. Proving loops properties requires constructing a loop invariant. The loop invariant is often the inductive property one has to prove of a recursive program that is equivalent to a given loop.

According to Rice Theorem, every interesting question about the behavior of programs is undecidable (1953). Software verification problem is undecidable; so it is not possible to talk about NP-completeness which is valid for only decidable ones. Although problems related with the behaviors of programs are undecidable, they are classified as recognizable. This means, we can get answered if the answer is true. The problem is asking the right question.

Software verification is the act of proving or disproving the correctness of an abstract model that will be realized against its formal specifications. It provides the answer to the question: “Are we building the product right?” There are two methods of verification: Theorem proving and model checking.

Theorem proving is a technique where both the system and its desired properties expressed as mathematical logic formulas. The logic is given by a formal system, which defines a set of axioms and a set of inference rules. Then, theorem proving is the process of finding the proof of property from the axioms of the system by applying inference rules. Steps in the proof appeal to the axioms and rules, and possibly derived definitions and intermediate lemmas. Although the proof could be constructed by hand, since systems becoming large and complex, it is not reasonable. Hence, there has been a great effort on developing theorem provers with various degree of automation, and also proof checkers have been proposed to confirm the correctness of the proof. Another way is the interactive theorem prover. By definition, it requires human assistance which causes the process to be slow, and error-prone. Prolog is the commonly used tool for theorem proving.

Model checking is a widely used verification technique that is model-based, automated, using a property verification approach, mainly useful for verifying concurrent and reactive systems, typically in a post development stage. The overall behavior of a distributed system is modeled as a transition system, whose states represent the global states of the distributed system, and whose transition relation gives the possible evolutions of the system. It can be checked whether such a transition system is a model of a temporal logic formula. There are several tools used in industry. SPIN performs software verification at design time over its programming language called Promela. Also JavaPathFinder verifies java code. You add a special class (Verify) inside your java code.

In contrast to the theorem proving model checking is completely automatic and fast. Model checking is used to check partial specifications; therefore it can provide useful information about a system’s behavior without checking the whole system. Above all, model checking outputs counterexample if the given property doesn’t hold by the model, which usually represents the subtle errors in design, and thus can be used to help in debugging.

It might be possible to find some software bugs by using verification either using theorem proving or model checking. But it is not possible to find all. Same thing is valid for defects. Also Dijkstra supported my idea in 1972: “Program testing can be used to show presence of the bugs, but never to show their absence”

In conclusion, this problem is undecidable but recognizable. It is possible to verify a software product under some conditions. This does not conflicts with undecidability, as undecidability is defined each element inside domain. This problem is undecidable and the answer of the question is not yes for each software product.

JSON & Security Vulnerabilities

JSON (JavaScript Object Notation), iki farklı sistem arasında veri değişimi için kullanılan bir formattır (biçimdir). Temel olarak nesnelerin insanlar tarafından okunabilir bir formatta transfer edilmesini sağlamaktadır. AJAX ile birlikte kullanılmaya başlayan bu yöntem 2002 yılında Jeremy Damian Horn tarafından XML yerine alternatif olarak önerilmiştir. JSON biçiminin kuralları Douglas CrockFord tarafından düzenlenerek RFC 4627 standartıyla betimlenmiştir. Bu standarta göre application/json medya tipiyle tanımlanır.

JSON biçiminde Numeric, String, Boolean, Array, Object ve null veri tipleri tanımlanmıştır. Örneğin ürün isimlerinizin listesini JSON ile tanımlayabilirsiniz. Ürün listeniz bir array olacağından bunu JSON biçiminde "[" ile "]" arasında virgül ile ayrılmış String'ler halinde yazabilirsiniz.

    {
        "items": [
        "Ürün Adı 1",
        "Ürün Adı 2",
        "Ürün Adı 3",
        "Ürün Adı 4",
        "Ürün Adı 5" ]       
    }
   

Bu tanımlamaya göre çalışma zamanında bir nesne oluşturabiliriz. Bunun için yukarıdaki tanımlamanın string olarak bir JSON_CodeText isminde bir değişkende tanımlandığını kabul edelim.

var products = eval("(" + JSON_CodeText + ")" )

Bu işlemden sonra artık products.items[0] gibi basit bir kod parçacığıyla bu listeye erişebiliyoruz. Buraya kadar JSON'ın nasıl bir biçim olduğunu öğrendik. Şimdi isterseniz bunun AJAX ile nasıl kullanıldığını inceleyelim. Aşağıdaki kod parçacığını inceleyelim.

var the_object;
var http_request = new XMLHttpRequest();
http_request.open("GET", url, true);
http_request.onreadystatechange = function () {
    if (http_request.readyState == 4) {
        if (http_request.status == 200) {
            the_object = eval("(" + http_request.responseText + ")");
        } else {
            alert("There was a problem with the URL.");
        }
        http_request = null;
    }
};

Buraya kadar her şey gayet güzel gözüküyor. JSON içeriğini sunucudan indirerek çok güzel Ajax uygulamaları geliştirebilirsiniz. XML'in tag'lemesinin getirdiği hantallıktan
kurtulabiliriz. Üstelik istemci tarafında kendi özel nesnelerimizi kullanabilir, nesneye dayalı programlamaya daha yakın bir yazılım geliştirme yaklaşımından bulunabiliriz.

Fakat size bir kötü haberim var !! Bu yöntem yeterince güvenli değildir. HTML'deki <script> tag'i için tüm internet tarayıcıları "aynı kaynak politikası" nı uymamaktadır. Başka bir sitedeki zarar vermeyi amaçlayan bir sayfa başka bir sayfadaki JSON nesnesine erişebilir. Saldırgan başka bir sitedeki JSON nesnesinin içeriğini görebilir. Özellikle dizi kullanımlarında bu tür saldırılar yapılabiliyor. Burada ince detayları veremeyeceğimiz yöntemle
saldırgan Array() prototype'ini override ederek tüm içeriği görebilir ve kendisine gönderebilir. Üstelik bunu sizin güvenilir olarak gördüğünüz siteye ait pencere üzerinden yapabilir.

SSL çok güvenli bir iletişim metodolojisi olarak söylense de, SSL sadece istemci ile sunucu arasındaki trafiğin güvenli olmasını sağlar. Oysa ki, günümüzdeki bütün truva atları istemci tarafında açık olarak bulunan içerik üzerine saldırmaktadırlar. JSON ile iletişim kuran güvendiğiniz siteden gelip giden bilgiyi başka bir kod tarafından alınabilir. Üstelik o penceredeki haklar ile bu işlem yapılabilir.

Bu saldırı türüyle ilgili bir kaç savunma yöntemi önerilmiştir. Ancak bunlar kalıcı olmayan çözüm önerileridir (pseudo remedy). Bu yöntemlerden ilki tüm JSON tanımlarınızı /* ile */ arasına almak ve saldırgan eval ile nesneyi oluşturmak istediğinde elinde bir nesne olmamasını sağlamaktır. Saldırgan bunu boş string olarak görecektir. Ancak siz bu kodu işlerken başında bu yorum işaretlerini kaldırıp eval yapabilirsiniz. Kaldı ki bu yöntemin kullanımının yaygınlaşmasıyla, bunu saldırgan da yapabilecektir.

XML, JSON'dan farklı olarak bir işaretleme dilidir (markup language). JSON sadece transfer edilecek veriyi ifade etme şeklidir. Bu yüzden JSON için XML'deki gibi bir geçerlilik kontrolü yapmak mümkün olmuyor. JSON her ne kadar programcı açısından daha cazip gözükse de saldırılara olan zayıflığı sebebiyle çok fazla tercih edilmemesi gereken bir veri değişim biçimidir.

Windows Vista Gadget: Digital Clock

Bu yazımızda Microsoft Windows Vista ile hayatımıza hızlı bir giriş yapan Gadget kodlamasından bahsedeceğiz. Örnek bir gadget olarak dijital saati geliştireceğiz.

Müfettiş Gadget ile hayatımıza merhaba diyen gadget kelimesinin tam anlamı da aslında çizgi filmdeki o karakterden çok da farklı değildir. Gadget aslında hayatımızı kolaylaştırmak için yapılan cihazlara verilen genel bir addır. Örneğin, tuttuğunuzda bir lazer ışık yayan bir anahtar karanlıkta da kapınızı açmanızı sağlayacaktır. Yine benzer bir terim de gizmo'dur. Gizmo de gadget ile benzer bir tanımlamaya sahiptir. Tek farkı gizmo'ların hareket eden parça(cık)lar içermesidir. Bu tanımlamaya göre aslında dijital saat bir gadget iken analog bir saat (hareket eden bir akrep ve yelkovan olduğu için ) gizmo'dur.

Ancak bizim bu makalede bahsediğimiz gadget Microsoft Windows Vista ile hayatımıza giren ve tam tanımındaki hayatımızı kolaylaştıran Windows Sidebar üzerinde yer alan gadget'lardır. Gadget aslında bir dizi html, xml, js ve resim dosyalarından oluşan
bir klasördür. Bu yazımızda sizinle birlikte dijital saat (her ne kadar dijital
saat tanımı gereği gizmo olsa da) gadget'i geliştireceğiz.

Öncelikle gadget'imizin yer alacağı dizine gidelim. Bunun için çalıştır'a aşağıdaki
dosya yolunu yazıp boş bir klasör oluşturalım.

%userprofile%\AppData\Local\Microsoft\Windows Sidebar\Gadgets

Windows ile gelen varsayılan gadget'lar Program Files altında yer almasına karşın
biz sadece kendi kullanıcımız tarafından kullanılacak bir gadget oluşturacağız.

Gadget'i oluşturmak için en kolay yöntem'i uygulayacağız. Bunun için bir xml ve
bir html dosyası yeterli olacaktır. Öncelikle xml dosyamızı oluşturalım. Xml dosyasının
ismi gadget.xml olmak zorundadır. Windows Sidebar buna göre neyi yükleyeceğini bilmektedir.
Bir de aşağıda da görebileceğiniz gibi bu xml gadget hakkında bilgileri içermektedir.

<?xml version="1.0" encoding="utf-8" ?>
<gadget>
    <name>Sample Digital Clock</name>
    <namespace>Microsoft.Academic</namespace>
    <version>1.0.0.0</version>
    <author name="Yunus Emre ALPÖZEN">
        <info url="www.msakademik.net" />
    </author>
    <copyright>&#169; 2007</copyright>
    <description>My first gadget</description>
    <hosts>
        <host name="sidebar">
            <base type="HTML" apiVersion="1.0.0" src="digitalClock.html" />
            <permissions>Full</permissions>
            <platform minPlatformVersion="1.0" />
        </host>
    </hosts>
</gadget>

Şimdi de gadget.xml dosyasında referans verdiğimiz digitalClock.html dosyasını oluşturalım. Bu kodun açıklamasını yapma gereği bile duymuyorum. Gayet standart bir html kodudur.

<html>
<head>
    <title>Hello, World!</title>
    <style>
        body
        {
            margin: 0;
            width: 130px;
            height: 20px;
        }
        #gadgetContent
        {
            width: 130px;
            top: 15px;
            text-align: center;
            font-family: Tahoma;
            font-size: 10pt;
            position: absolute;
        }
    </style>
</head>
<body bgcolor="black">
    <table id="gadgetContent" cellpadding="0" cellspacing="0" border="0">
        <tr>
            <td bgcolor="black">
                <img src="imgs/dg8.gif" id="hr1" />
                <img src="imgs/dg8.gif" id="hr2" />
                <img src="imgs/dgc.gif" />
                <img src="imgs/dg8.gif" id="mi1" />
                <img src="imgs/dg8.gif" id="mi2" />
                <img src="imgs/dgc.gif" /><img src="imgs/dg8.gif" id="ss1" />
                <img src="imgs/dg8.gif" id="ss2" />
                <img src="imgs/dgpm.gif" id="ampm" />
            </td>
        </tr>
    </table>
</body>
</html>

<script language="javascript">
function fn_getTime(){
    var hr, mi ,ss, am_pm, timeStr
    now = new Date()
    hr= now.getHours()+100;
    mi= now.getMinutes()+100;
    ss= now.getSeconds()+100;
  
    if(hr==100){hr=112;am_pm='am';}
    else if(hr<112){am_pm='am';}
    else if(hr==112){am_pm='pm';}
    else if(hr>112){am_pm='pm';hr=(hr-12);}
    timeStr= ""+hr+mi+ss;
    hr1.src="imgs/dg" + timeStr.substring(1,2) + ".gif";
    hr2.src="imgs/dg" + timeStr.substring(2,3) + ".gif";
    mi1.src="imgs/dg" + timeStr.substring(4,5) + ".gif";
    mi2.src="imgs/dg" + timeStr.substring(5,6) + ".gif";
    ss1.src="imgs/dg" + timeStr.substring(7,8) + ".gif";
    ss2.src="imgs/dg" + timeStr.substring(8,9) + ".gif";
    ampm.src ="imgs/dg" +am_pm + ".gif";
  
    window.setTimeout(fn_getTime,1000);
}
//fn_getTime();
</script>

Tabi ki de bu örneği çalıştırabilmeniz imgs klasörüne sahip olmanız ve altında dg1.gif, dg2.gif... gibi rakamları içeren imaj dosyalarına sahip olduğunuzu kabul ediyoruz. Bu örneğimizi buradan indirebilirsiniz.
Sonuçta aşağıdaki gibi bir gadget'a sahip olacağız.



Aynı şekilde AJAX kullanarak dinamik içerik gösteren bir gadget da hazırlayabilirsiniz. Gadgetler ile yapabilecekleriniz hayal gücünüzle sınırlıdır :)