Runtime Verification

General Information

Runtime Verification on laskennallisen järjestelmän analysoinnin ja suorituksen menetelmä, joka on suunniteltu poimimaan tietoa käynnissä olevasta järjestelmästä ja havaitsemaan ja mahdollisesti reagoimaan siihen, vastaako havaittu käyttäytyminen tiettyjä ominaisuuksia tai rikkoo niitä. Tätä tekniikkaa voidaan käyttää useisiin tarkoituksiin, kuten turvallisuus- tai turvallisuuspolitiikan seurantaan, vianetsintään, testaukseen, varmistukseen, validointiin, suoritusanalyysiin, vikaturvallisuuteen, käyttäytymisen muuttamiseen ja muihin. Se välttää perinteisten muodollisten varmennustekniikoiden monimutkaisuuden analysoimalla pientä määrää suorituspolkuja ja työskentelemällä suoraan varsinaisen järjestelmän kanssa.

Runtime Verification Inc. on yritys, joka on keskittynyt virtuaalisiin kone- ja älykkäisiin sopimusturvallisuustarkastuksiin, joissa käytetään ajoajan varmennustekniikoita. Niiden tarjoamia palveluita ovat muun muassa suunnitteluarvostelut, koodiarvostelut, auditoinnit sekä älykkäiden sopimusten ja protokollien muodollinen varmentaminen.

Mitä tuotteita Runtime Verification Inc tarjoaa tällä hetkellä?

Runtime Verification Inc. kehittää parhaillaan kolmea ydintuotetta: RV-Predict on ennakoiva ajonaikainen analysointityökalu, joka keskittyy ohjelman samanaikaisten virheiden automaattiseen havaitsemiseen. RV-Monitor on kehitysmetodologia ja kirjaston luontityökalu, jonka avulla käyttäjän valitsemia ominaisuuksia voidaan seurata ja suorittaa ajon aikana. RV-Match on työkalu, jonka avulla tyhjentävä ajoajan validointi voidaan suorittaa symbolisesti kaikilla mahdollisilla ohjelmareiteillä ja osoittaa siten, että tietyt ominaisuudet ovat oikeita kaikille tietyn ohjelman mahdollisille suorituksille.

Milloin ja miksi RV-Predictiä pitäisi käyttää?

Aina kun samanaikaisuuden oikeellisuus on tärkeää monisäikeisille sovelluksille, tulee käyttää RV-Predictiä. RV-Predict kykenee havaitsemaan tehokkaasti ja saumattomasti samanaikaisuusongelmat ja dataklauksen ohjelmassa, on hyvin helppo ajaa eikä yleensä vaadi mitään asetuksia. RV-Predict käyttää myös ainutlaatuisia ennustusominaisuuksia havaitsemaan mahdollisia väittämiä, vaikka niitä ei esiintyisikään RV-Predict-tietueiden suoritusjäljessä.

Milloin ja miksi RV-Monitoria pitäisi käyttää?

RV-Monitor mahdollistaa monimutkaisten sovellusten tai järjestelmien tarkkailun ja niiden jäljitysominaisuuksien suorittamisen. RV-Monitoria tulee käyttää niin kauan kuin ohjelmakehityksen hallintaan on spesifikaatio, ja tämän spesifikaation noudattaminen on ohjelmiston kriittinen ominaisuus. RV-Monitorin avulla voidaan myös seurata yleisten sovellustunnisteiden noudattamista, mukaan lukien Android ja Java API.

< Milloin ja miksi RV-Matchia pitäisi käyttää?

RV-Monitor voi varmentaa ja valvoa tiettyjen ohjelman suorituksen ominaisuuksien noudattamista, kun taas RV-Match voi todistaa ohjelman oikeellisuuden ajonaikaisesti, analysoimalla näin suoritusjälkiä kaikilla mahdollisilla suoritusreiteillä ja kaikilla mahdollisilla syötteillä. RV-Match tarjoaa vahvat oikeellisuustakuut, simuloiden suoritusta symbolisella tavalla käyttämällä kohdekielen virallisesti määriteltyä semantiikkaa. Kun vaaditaan vahvat muodollisen validoinnin takeet, RV-Matchia tulisi käyttää, ja sitä voidaan käyttää myös RV-Monitorin kanssa poistamaan seuranta alueilla, jotka voivat todistaa, että ominaisuuksia ei ole koskaan loukattu.

<

Mitkä lisenssit Runtime Verification Inc: n tuotteet kattavat?

RV: n kehittämät hankkeet jakautuvat kahteen luokkaan: patentoidut tuotteet ja avoimella lisenssillä lisensoidut tuotteet (osana RV: n avoimen lähdekoodin ekosysteemiä).

Pakolliset tuotteet käsittävät kaikki tuotteet, joita ei ole nimenomaisesti lisensoitu avoimella lisenssillä ja joita käytetään ainoastaan arviointitarkoituksiin ja akateemisiin / ei-kaupallisiin tarkoituksiin. Jälkiperäisteoksia ei saa luoda käyttämällä matkailuautojen patentoituja tuotteita ilman ennakkolupaa, ja RV varaa kaikki oikeudet omistusoikeuden alaisiin tuotteisiin. Tuotteita ei saa millään tavalla kääntää.

Blockchain-hanke Tarkastus

Käytönaikainen varmennus on ollut mukana useiden lohkoketjuhankkeiden tarkastuksessa, mukaan lukien muun muassa seuraavat:

- Älykkäiden sopimusten turvatarkastus: Ne suorittavat edullisia sopimusten tarkastuksia, kuten ERC-20, ERC-721, ERC-4626 jne.

- Protokollien turvatarkastus: Sisältää lainanantoon liittyviä toimia koskevat protokollat.

- Muodollinen varmennus: Tarjoaa avoimen lähdekoodin muodollisia varmennus- ja kehitystyökaluja tarkastuskustannusten vähentämiseksi ja jatkuvan virallisen varmennuksen mahdollistamiseksi.