References of "Vukotic, Ivana 50022238"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailAsphalion: Trustworthy Shielding Against Byzantine Faults
Vukotic, Ivana UL; Rahli, Vincent UL; Verissimo, Paulo UL

in Vukotic, Ivana; Rahli, Vincent; Verissimo, Paulo (Eds.) Asphalion: Trustworthy Shielding Against Byzantine Faults (2019)

Detailed reference viewed: 40 (9 UL)
Full Text
Peer Reviewed
See detailVelisarios: Byzantine Fault-Tolerant Protocols Powered by Coq
Rahli, Vincent UL; Vukotic, Ivana UL; Volp, Marcus UL et al

in ESOP 2018 (2018, April)

Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended efforts to ensure the correctness and security of these ... [more ▼]

Our increasing dependence on complex and critical information infrastructures and the emerging threat of sophisticated attacks, ask for extended efforts to ensure the correctness and security of these systems. Byzantine fault-tolerant state-machine replication (BFT-SMR) provides a way to harden such systems. It ensures that they maintain correctness and availability in an application-agnostic way, provided that the replication protocol is correct and at least n-f out of n replicas survive arbitrary faults. This paper presents Velisarios a logic-of-events based framework implemented in Coq, which we developed to implement and reason about BFT-SMR protocols. As a case study, we present the first machine-checked proof of a crucial safety property of an implementation of the area's reference protocol: PBFT. [less ▲]

Detailed reference viewed: 412 (56 UL)
Full Text
Peer Reviewed
See detailFormally Verified Differential Dynamic Logic
Bohrer, Brandon; Rahli, Vincent UL; Vukotic, Ivana UL et al

in CPP 2017 (2017)

Detailed reference viewed: 270 (53 UL)