1. Improved formal verification of SDN-based firewalls by using TLA+Tatjana Kapus, 2023, original scientific article Abstract: In an article published in IEEE Access in 2020, researchers present an approach to using TLA + for the formal verification of whether a network of SDN (Software-Defined Networking) switches implements the filtering rules of a given monolithic firewall. The distributed as well as monolithic firewalls are specified with TLA + . It is shown that the correctness of the former with respect to the latter can be verified automatically by using the TLC model checker. The main contributions of this paper are the following improvements of that approach. Firstly, by specifying switches without using any variables, the time needed for the model checking is reduced significantly. For example, the verification of the same networks takes a few seconds with the new approach and does not end after several hours with the previous one. Secondly, the following problem is solved. With the latter, if a monolithic firewall allows a packet to pass through, all the paths in the distributed firewall which the packet is routed on must allow the same. Otherwise, the model checker proclaims the distributed firewall to be in error. We present an additional approach to the verification, which gives a positive answer if at least one of the paths allows the packet to pass through.
Keywords: firewalls, formal specification, formal verification, logic, model checking, software defined networking
Published in DKUM: 04.12.2023; Views: 285; Downloads: 22
 Full text (1,24 MB)
This document has many files! More... |
2. OBLIČJE ZA SIMULATOR OPTIČNIH OMREŽIJEnej Unterajter, 2018, diploma project paper Abstract: V sklopu projekta smo napisali program v programskem jeziku C++, ki omogoča uporabniku lažje delo s simulatorjem optičnih omrežij Hegons. Program smo pisali v okolju Microsoft Visual Studio. Za izvedbo smo se natančneje seznanili z delovanjem in uporabo programa Hegons, spoznali pa smo še knjižnico FLTK in program gnuplot, ki smo ju uporabili za izvedbo grafičnega vnosa podatkov oziroma prikaza rezultatov. V poročilu bomo v začetku predstavili težave, ki so se pojavljale pri uporabnikih programa Hegons, nato pa predstavili uporabljene programe ter izvedbo in delovanje izdelanega programa.
Keywords: komunikacijsko omrežje, simulacija, programiranje, grafični uporabniški vmesnik
Published in DKUM: 05.02.2019; Views: 1936; Downloads: 96
Full text (1,34 MB)
This document has many files! More... |
3. Zagotavljanje skladnosti v porazdeljeni krmilni ravnini programsko določenih omrežijSimon Malek Kuzmič, 2018, master's thesis Abstract: Magistrsko delo zajema kratek opis konceptov in arhitekture programsko določenih
omrežij. Sledita opis porazdeljene izvedbe krmilne ravnine in predstavitev glavnih pristopov
zagotavljanja skladnosti v omrežjih s tako ravnino. Magistrsko delo se osredotoča na
zagotavljanje skladnosti v omrežjih s krmilniki ONOS. Namen je predstavitev delovanja teh
krmilnikov v grozdu in način zagotavljanja skladnosti njihovih informacij o topologiji
omrežja. Delovanje grozda smo preizkusili v različnih scenarijih v navideznih omrežjih,
tvorjenih z emulatorjem Mininet.
Keywords: programsko določeno omrežje, krmilnik, grozd, skladnost
Published in DKUM: 30.11.2018; Views: 1202; Downloads: 119
Full text (2,78 MB) |
4. Izboljšanje uporabniške izkušnje IPTV z daljinsko prilagoditvijo parametrov povezave xDSLGregor Pavlovič, 2018, undergraduate thesis Abstract: V teoretičnem delu diplomske naloge so predstavljene tehnologije DSL in storitev televizije IP ter orodja in postopki, s katerimi telekomunikacijski operater zazna težave pri storitvi televizije IP, ponujani preko DSL. V praktičnem delu je poudarek na konfiguriranju linijskih parametrov povezave DSL za zagotovitev kakovosti izkušnje storitve televizije IP. Uporabljena sta testna priključka DSL Telekoma Slovenije. Prvi testni priključek je uporabljen za predstavitev operaterjevih orodij, drugi pa za predstavitev konfiguriranja naročniškega priključka.
Keywords: digitalni naročniški vod, televizija IP, kakovost izkušnje
Published in DKUM: 08.11.2018; Views: 1172; Downloads: 79
Full text (1,69 MB) |
5. Tvorjenje avtomatov linearnih končnih prič za formule ACTLW z orodjem ESTRok Vogrin, 2018, master's thesis Abstract: Magistrsko delo obravnava tvorjenje avtomatov linearnih končnih prič veljavnosti formul akcijske logike dreves izvajanj z operatorjem unless (ACTLW -- Action-based Computation Tree Logic with Unless operator) v modelih realnih sistemov, imenovanih označeni sistemi prehajanja stanj. Namen dela je tvorjenje avtomatov prič, ki kažejo, kako so v takem modelu prisotne lastnosti, opisane z veljavno formulo ACTLW. V prvem delu naloge so predstavljeni ključni elementi za tvorjenje avtomatov prič. Vpeljana sta pojma karakteristična funkcija in binarni odločitveni graf. Definirani so označeni sistemi prehajanja stanj, končni avtomati ter logika ACTLW. V drugem delu je na podlagi definicij razvit postopek in opisana implementacija tvorjenja avtomatov linearnih končnih prič z orodjem EST. Tvorjenje avtomatov je prikazano na primeru modela komunikacijskega protokola z omejenim številom ponovnih oddaj in biološkega sistema uravnavanja laktoznega operona.
Keywords: formalne metode, preverjanje modelov, temporalna logika, avtomati prič, simbolične metode
Published in DKUM: 09.10.2018; Views: 1477; Downloads: 158
Full text (666,65 KB) |
6. IZRECNO OBVEŠČANJE O ZAMAŠITVI V OMREŽJIH IPAlen Bezenšek, 2018, diploma project paper Abstract: V projektu smo se ukvarjali z izrecnim obveščanjem o zamašitvi v omrežjih IP. Najprej smo proučili delovanje te metode in kako je podprta v različnih operacijskih sistemih. V nadaljevanju smo s pomočjo analizatorja prometa Wireshark zajemali promet pri dostopanju do spletnih strani in ga analizirali glede izrecnega obveščanja o zamašitvi. V programskem okolju Rivebed Modeler smo modelirali in simulirali omrežja z uporabo izrecnega obveščanja o zamašitvi in brez njega. Rezultate smo primerjali ter razlike komentirali in grafično prikazali. Nazadnje so na kratko podane še ključne ugotovitve projekta.
Keywords: izrecno obveščanje o zamašitvi, simulacija, analiza prometa, protokol za nadzor prenosa, medmrežni protokol
Published in DKUM: 24.05.2018; Views: 1493; Downloads: 106
Full text (1,34 MB) |
7. Avtomatizacija analize povezav TCPAljaž Gaber, 2017, diploma project paper Abstract: V projektu smo se ukvarjali z avtomatizacijo analize povezav protokola TCP. Za analizo smo uporabili program tshark, ki je terminalska različica analizatorja protokolov Wireshark. Analiza je avtomatizirana s pomočjo skripta, napisanega v lupini Windows PowerShell. Za izvedbo projekta smo se podrobneje seznanili z delovanjem protokola TCP. V programskem delu je bilo treba spoznati tshark in principe pisanja skriptov v PowerShellu. Celoten razvoj skripta je potekal v razvojnem okolju Windows PowerShell ISE. V tem poročilu je najprej predstavljen problem, nato na kratko protokol TCP, Wireshark in PowerShell. Nazadnje je razložena celotna izvedba in delovanje našega skripta.
Keywords: protokol za nadzor prenosa, analiza omrežnega prometa, protokolni analizator, skript
Published in DKUM: 26.01.2018; Views: 1979; Downloads: 101
Full text (1,40 MB) |
8. Simulations of VoIP applications in INET frameworkSebastijan Horvatić, 2017, master's thesis Abstract: This master's thesis describes the support for modelling Voice over Internet Protocol (VoIP) applications in the INET Framework. First, it briefly presents the VoIP technology and factors responsible for the VoIP quality of service. Next, the thesis moves on to discuss the OMNeT++ environment and the INET Framework, their installation and usage. Following this, it examines all of the INET packages and modules available for VoIP modelling, with all VoIP-related INET examples then shortly described and tested. By using INET, our own network and application models are created and simulated using different parameters. Comparisons of the simulation results are carried out and some of the best-found parameters for the VoIP communications are presented. At last, the calculation of jitter by using the obtained simulation results and Excel program is described, because jitter is not shown in the simulation results in INET.
Keywords: voice over internet protocol, performance analysis, simulation, real-time transport protocol, user datagram protocol
Published in DKUM: 18.08.2017; Views: 1559; Downloads: 140
Full text (3,86 MB) |
9. Akcijska logika dreves izvajanj z operatorjem unless : doktorska disertacijaRobert Meolic, doctoral dissertation Abstract: Doktorska disertacija definira in raziskuje akcijsko logiko dreves izvajanj z operatorjem unless (ACTLW). ACTLW je izjavna temporalna logika razvejanega časa. Izhaja iz logike ACTL, ki je bila vpeljana leta 1990 in je ena od uveljavljenih temporalnih logik za izražanje lastnosti modelov, ki temeljijo na dogodkih. ACTLW je fleksibilnejša od ACTL, saj ne vsiljuje uporabe notranjega dogodka T pri izražanju lastnosti. ACTLW je tudi nekoliko izraznejša od ACTL, saj vsebuje temporalni operator unless (W), katerega pomena v ACTL ni možno v celoti izraziti. Nasprotno pa lahko vse formule ACTL izrazimo z uporabo operatorjev ACTLW. ACTLW omogoča učinkovito izvedbo preverjanja modelov s podobnimi algoritmi kot pri preverjanju modela s CTL, kar je pomembna izboljšava glede na logiko ACTL. Doktorska disertacija podaja definicijo logike ACTLW, izpeljave vseh standardnih temporalnih operatorjev in algoritme za globalno preverjanje modela z ACTLW s simboličnim računanjem. Predstavljeni so tudi algoritmi za tvorjenje diagnostike pri ACTLW, za tvorjenje lineamih prič in protiprimerov pri ACTLW ter za tvorjenje avtomatov prič in proti primerov pri ACTLW. Doktorska disertacija je v celoto zaokrožena z vzorci formul ACTLW in dvema večjima praktičnima primeroma: verifikacijo več različnih algoritmov za medsebojno izključevanje in verifikacijo dveh asinhronih vezij za porazdeljeno medsebojno izključevanje.
Keywords: formalne metode verifikacije sistemov, preverjanje modela, temporalna logika, doktorske disertacije, CTL, ACTL, ACTLW, diagnostika, problem medsebojnega izključevanja
Published in DKUM: 04.08.2017; Views: 1995; Downloads: 125
Full text (1,04 MB) |
10. Preverjanje pravilnosti obnašanja sistemov s sočasnostjo : magistrsko deloRobert Meolic, master's thesis Abstract: Magistrsko delo obravnava metode preverjanja pravilnosti obnašanja sistemov, ki temeljijo na opisu sistema s procesno algebro. Podana je definicija procesne algebre in primeri opisov sistemov s procesi. Predstavljeno je ugotavljanje ekvivalence sledi, stroge, vejitvene in šibke opazovalne ekvivalence, ugotavljanje testne ekvivalence ter simbolično preverjanje modelov z izjavno vejitveno temporalno logiko ACTL. Vse obravnavane metode se med seboj odlično dopolnjujejo in skupaj tvorijo močno orodje za formalno verifikacijo sistemov. V magistrskem delu je opisana izvedba takšnega orodja z BDD-ji. Uporaba orodja je ponazorjena na primeru verifikacije komunikacijskega protokola BRP.
Keywords: formalne metode verifikacije, sistemi s sočasnostjo, procesne algebre, opazovalne ekvivalence, testne ekvivalence, simbolično preverjanje modelov, ACTL, BDD
Published in DKUM: 04.08.2017; Views: 2558; Downloads: 96
Full text (1,10 MB) |
