Luin Vastaamon tietomurroista. Onko nykyään mahdollista rakentaa ohjelmistoja siten, että ne todistettaisiin bugittomiksi? Paljonko tällaisen käyttöjärjestelmän tekeminen veisi aikaa? Ilmeisesti proof driven development ei ole yleisesti käytössä.
Tuossa ei mahdollisesti ollut edes kyse ohjelmointivirheestä, jossa tapauksessa ohjelmiston oikeaksi todistaminen ei olisi asiaan auttanut.
Eli siis jos esimerkiksi palvelimelle on määritelty täydet oikeudet kaikkiien tietoihinj käyttäjälle, jonka tunnus on root ja salasana root, niin silloin ko. käyttäjätunnuksella tuolle palvelimelle kirjautumalla pääsee kaikkiin tietoihin, vaikka ohjelma toimiikin virheettömästi.
Yleisesti ottaen jos todistetaan ohjelmistoa oikein toimivaksi, niin mihin nähden? Entä jos vaatimusmäärittely on huono?
Aina ei asiakas oikein ymmärrä tietotekniikasta ja olen kerran työrmännyt ongelmaan, että yleisesti on väliaikainen vika operaattorin verkossa, jonka takia kenenkään Internet-yhteydet eivät toimi kunnolla ja asiakas ei tätä usko ja syyttää ohjelmiston tekijää siitä että se on viallinen kun se ei lataudu tarpeeksi nopeasti www-selaimella ja on mahdoton käyttää. Ja uhkailee jopa korvausvaatimuksilla väärää yritystä. Ja näissä kuvioissa ei kukaan tunnusta mitään ei operaatori eikä web-hotelli.
Noita asioita taklataan valvonnoilla. Aika yleistä on, että esim. prometheus tai vastaava on valjastettu keräämään tietoa ja toimimaan valvontayksikkönä niin palvelimen metriikoille, itse palveluille, kuin verkoillekkin. Vikatilanteen sattuessa (vaikka verkkovika tai yhteys ei muodostu palveluun x) ylläpito saa tästä hälytyksen ja SLA:n puitteissa alkaa selvittelemään tilannetta.
(Yritetään pysyä aiheessa; walkoutin juttu meni taas ihan eri asiaan, josta voi halutessaan avata ihan uuden keskustelun.)
Jaska kirjoitti:
Onko nykyään mahdollista rakentaa ohjelmistoja siten, että ne todistettaisiin bugittomiksi?
Ihminen on vastuussa ohjelman toimintalogiikasta, ja sitä ei voi koneellisesti osoittaa virheettömäksi, ennen kuin tekoäly oppii ymmärtämään asioiden todellista tarkoitusta (eikä tee virheitä siinä). Jos ohjelmaan on tehty järjestely, jossa kuka tahansa voi hakea mitä tahansa tietoa, tietokone ei voi päättää, onko se bugi vai ominaisuus.
Yksittäisiä bugin tyyppejä voidaan koneellisesti etsiä. Toisaalta mikään ratkaisu tässä ei ole täydellisen varma, vaan kyse on aina karkeasta arvauksesta. Etsintää voi tehdä koodin tasolla tai testaamalla.
Hyvä esimerkki ovat SQL-injektiot eli turvattomat tietokantakyselyt: Automaattisella työkalulla voidaan testata eri syötteitä nettisivuston kaikille lomakkeille, jolloin voidaan huomata, jos tiettyjä merkkejä sisältävillä syötteillä saadaan aivan erilainen sivu. Toisaalta tämä löytää vain tyypilliset bugit; aina voi tehdä erikoisemman bugin, jota ei huomata testissä. Koodista voidaan myös tunnistaa tilanne, jossa käyttäjän syöttämä teksti päätyy tietokantakyselyyn ilman mitään käsittelyä. Toisaalta jos syöte käsitellään jollain tavalla, onkin jo paljon vaikeampi selvittää, onko se käsittely juuri kyseisessä tilanteessa riittävä. Asiaa on varmasti mietitty jo parikymmentä vuotta ja käsitelty esimerkiksi PHP-kielen kehittäjäyhteisössä, ja edelleenkään SQL-aukkojen tunnistamiseen koodista ei ole tyydyttävää automaattista järjestelmää.
Tiettyjä bugeja vastaan taistellaan myös uusilla ohjelmointikielillä. Esimerkiksi C-kielellä on tehty paljon virheitä muistin käsittelyssä, ja Rust-kielessä tietyt muistiin liittyvät asiat on pakko tehdä tarkkojen sääntöjen mukaan, jotta näitä virheitä ei olisi mahdollista tehdä.
Metabolix kirjoitti:
edelleenkään SQL-aukkojen tunnistamiseen koodista ei ole tyydyttävää automaattista järjestelmää.
Periaatteessa voitaisiin tehdä tarkistus, että itse kyselynä menee vain vakiomerkkijonoja ja kaikki ohjelman saama syöte menee parametreina.
Tämä toki tarkoittaisi, että muuten kuin parametrisoituna kyselynä tehtävä, syötettä sisältävä tietokantakysely aiheuttaisi virheen, olipa siinä sitten bugi tai ei.
Grez kirjoitti:
Periaatteessa voitaisiin tehdä tarkistus, että itse kyselynä menee vain vakiomerkkijonoja
Niin voitaisiin. Ongelmia tässä ratkaisussa ovat mm. useita valinnaisia ehtoja sisältävä hakulomake tai tulosten järjestely eri sarakkeiden mukaan. Näiden ongelmien takia vakiokyselyiden käyttöä ei pidetä yleisesti täysin tyydyttävänä ratkaisuna, mutta yksittäinen projekti saa tietysti tehdä asiasta oman päätöksensä.
Miten erotetaan syöte ja vakio? Ainoa aukoton rajaus olisi varmaankin se, että tiettyä funktiota (esim. SQL::query) saa kutsua vain siten, että parametri on suoraan lainausmerkeissä ilmoitettu vakio. Tämä johtaa juuri edellä mainittuihin vaikeuksiin erityistilanteissa. Jos halutaan hieman sallivampi lähestymistapa, joudutaan miettimään, onko vakio edelleen vakio, jos se sijoitetaan muuttujaan, välitetään funktiolle parametrina, yhdistetään toiseen vakioon, katkaistaan, valitaan ehtolauseella tms.
Vähänkin sallivampi vakion määritelmä johtaa kiinnostavaan mahdollisuuteen: Jos laitetaan taulukkoon ASCII-merkit vakioina, käydään läpi syötteen merkit ja yhdistetään taulukosta vastaavat vakiot, onko lopputulos vakio? Jos on, niin takuulla joku toteuttaa funktion juuri tätä varten, ja pian koodissa on uusi bugi nimeltä muuta_vakioksi($syöte).
Metabolix kirjoitti:
Miten erotetaan syöte ja vakio? Ainoa aukoton rajaus olisi varmaankin se, että tiettyä funktiota (esim. SQL::query) saa kutsua vain siten, että parametri on suoraan lainausmerkeissä ilmoitettu vakio.
Ei olisi mitenkään mahdotonta tehdä koneellinen analyysi siitä, voiko käyttäjältä saatavaa syötettä päätyä sql-kyselyihin vai ei.
Metabolix kirjoitti:
takuulla joku toteuttaa funktion juuri tätä varten, ja pian koodissa on uusi bugi nimeltä muuta_vakioksi($syöte).
No tässä nyt oli tarkoitus kai tehdä tyydyttävää automaattista tarkistinta, ei sellaista jota ei pysty kiertämään yrittämälläkään.
Toki ketjussa puhuttiin todistamisesta, eli jos tyydyttävä tässä yhteydessä tarkoittaa, että se pystyy todistamaan virheettömyyden, niin sitten olen samaa mieltä että lienee suht mahdotonta sellaisella tietokantakirjastolla joka antaa käyttäjän syöttää kyselyn SQL:nä.
Sinänsähän noita "useita valinnaisia ehtoja sisältävä hakulomake tai tulosten järjestely eri sarakkeiden mukaan" toimintoja voi toteuttaa muullakin tavalla kuin kirjoittamalla käsin SQL-kyselyitä.
Grez kirjoitti:
Toki ketjussa puhuttiin todistamisesta, eli jos tyydyttävä tässä yhteydessä tarkoittaa, että se pystyy todistamaan virheettömyyden, niin sitten olen samaa mieltä että lienee suht mahdotonta sellaisella tietokantakirjastolla joka antaa käyttäjän syöttää kyselyn SQL:nä.
Tällöin pitää tietysti olettaa aina, että syöte on potentiaalisesti vaarallinen -> ohjelma ei läpäise tarkistusta.
Aihe on jo aika vanha, joten et voi enää vastata siihen.