Consensus protocols are the core of modern blockchain systems, such as the Bitcoin, Ethereum, and Algorand networks. Thanks to these protocols, participants in a blockchain network can reach consensus on which blocks to add to a blockchain, to have a consistent chain of blocks in the whole network. Blocks are typically collections of transactions, e.g., transferring currency between participants, but can contain other data depending on the use case. Consensus protocols are difficult to design, test, and implement. Problems may only manifest in rare cases but can have disastrous consequences. Formal protocol models allow exhaustive analysis and formal verification. However, formal verification is only as good as the specification of the protocol. For example, specification properties could be vacuously true, or the specification may omit to mention liveness properties that are crucial for progress in a system implementation. This thesis describes the practical validation of a formal specification of Giskard, a consensus protocol used in the PlatON network. We translated key aspects of a formal model of Giskard in the Coq proof assistant to executable Python code, and integrated them into the Sawtooth blockchain framework. Then, we ran simulations of a blockchain network executing Giskard using Sawtooth, checking network node state properties of Giskard as well as its global safety properties. Automated clients from the Sawtooth network provided randomly generated transactions as input for the network. The implementation with the test results are available for reproducibility. Both consensus safety and liveness issues were found in the formal specification of Giskard during the simulations. Based on the previous informal English specification of Giskard, we propose a new formal specification which was validated to reach consensus on blocks in the simulated blockchain network and uphold the protocol’s crash and Byzantine failure tolerance to a certain degree. The improved formal model can serve as a new basis for verifying and implementing Giskard in the future. / Konsensusprotokoll utgör kärnan i moderna blockkedjesystem som Bitcoin-, Ethereum- och Algorandnätverken. Tack vare dessa protokoll kan deltagare i blockkedjenätverk nå konsensus om vilka block som ska läggas till, för att få en konsekvent blockkedja i hela nätverket. Block är vanligen samlingar av transaktioner, till exempel överföringar av valuta mellan deltagare, men kan också innehålla annan data beroende på användningsområdet. Konsensusprotokoll är svåra att designa, testa och implementera. Problem kanske bara visar sig i sällsynta fall, men kan ha katastrofala konsekvenser. Formella protokollmodeller tillåter uttömmande analys och formell verifiering. Men formell verifiering ger bara så goda resultat som protokollspecifikationen tillåter. Till exempel kan specfikationsegenskaper vara sanna innehållslöst eller så kan specifikationen underlåta att nämna framstegsegenskaper som är viktiga för att en systemimplementation inte ska låsa sig. Denna avhandling beskriver den praktiska valideringen av en formell specifikation av Giskard, ett konsensusprotokoll som används i PlatONnätverket. Vi översatte nyckelaspekter av en formell modell i bevisassistenten Coq till körbar Python-kod och integrerade koden i blockkedjeramverket Sawtooth. Sedan körde vi simuleringar av ett blockkedjenätverk som använder Giskard med hjälp av Sawtooth och undersökte Giskards tillståndsegenskaper för nätverksnoder och även dess globala säkerhetsegenskaper. Automatiserade klienter från Sawtooth-nätverket tillhandhöll slumpgenererade transaktioner som indata för nätverket. Implementeringen med testresultaten är tillgängliga för reproducerbarhet. Både säkerhets- och framstegsproblem hittades i den formella specifikationen av Giskard under simuleringarna. Baserat på en tidigare informell specifikation av Giskard på engelska föreslår vi en ny formell specifikation som validerades att nå konsensus på block i det simulerade blockkedjenätverket och att till en viss grad tolerera krascher och byzantinska fel. Den förbättrade formella modellen kan användas som en ny bas för att verifiera och implementera Giskard i framtiden.

In recent years, there have been incidents which decreased people's trust in some organizations and authorities responsible for ratings and accreditation. For a few prominent examples, there was a security breach at Equifax (2017), misconduct was found in the Standard & Poor's Ratings Services (2015), and the Accrediting Council for Independent Colleges and Schools (2022) validated some of the low-performing schools as delivering higher standards than they actually were. A natural solution to these types of issues is to decentralize the relevant trust management processes using blockchain technologies. The research problems which are tackled in this thesis consider the issue of trust in reputation for assessment and review credibility at different angles, in the context of blockchain applications. We first explored the following questions. How can we trust courses in one college to provide students with the type and level of knowledge which is needed in a specific workplace? Micro-accreditation on a blockchain was our solution, including using a peer-review system to determine the rigor of a course (through a consensus). Rigor is the level of difficulty in regard to a student's expected level of knowledge. Currently, we make assumptions about the quality and rigor of what is learned, but this is prone to human bias and misunderstandings. We present a decentralized approach that tracks student records throughout the academic progress at a school and helps to match employers' requirements to students' knowledge. We do this by applying micro-accredited topics and Knowledge Units (KU) defined by NSA's Center of Academic Excellence to courses and assignments. We demonstrate that the system was successful in increasing accuracy of hires through simulated datasets, and that it is efficient, as well as scalable. Another problem is how can we trust that the peer reviews are honest and reflect an accurate rigor score? Assigning reputation to peers is a natural method to ensure correctness of these assessments. The reputation of the peers providing rigor scores needs to be taken into account for an overall rigor of a course, its topics, and its tasks. Specifically, those with a higher reputation should have more influence on the total score. Hence, we focused on how a peer's reputation is managed. We explored decentralized reputation management for the peers, choosing a decentralized marketplace as a sample application. We presented an approach to ensuring review credibility, which is a particular aspect of trust in reviews and reputation of the parties who provide them. We use a Proof-of-Stake based Algorand system as a base of our implementation, since this system is open-source, and it has a rich community support. Specifically, we directly map reputation to stake, which allows us to deploy Algorand at the blockchain layer. Reviews are analyzed by the proposed evaluation component using Natural Language Processing (NLP). In our system, NLP gauges the positivity of the written review, compares that value to a scaled numerical rating given, and determines adjustments to a peer's reputation from that result. We demonstrate that this architecture ensures credible and trustworthy assessments. It also efficiently manages the reputation of the peers, while keeping reasonable consensus times. We then turned our focus on ensuring that a peer's reputation is credible. This led us to introducing a new type of consensus called "Proof-of-Review". Our proposed implementation is again based on Algorand, since its modular architecture allows for easy modifications, such as adding extra components, but this time, we modified the engine. The proposed model then provides a trust in evaluations (review and assessment credibility) and in those who provide them (reputation credibility) using a blockchain. We introduce a blacklisting component, which prevents malicious nodes from participating in the protocol, and a minimum-reputation component, which limits the influence of under-performing users. Our results showed that the proposed blockchain system maintains liveliness and completeness. Specifically, blacklisting and the minimum-reputation requirement (when properly tuned) do not affect these properties. We note that the Proof-of-Review concept can be deployed in other types of applications with similar needs of trust in assessments and the players providing them, such as sensor arrays, autonomous car groups (caravans), marketplaces, and more.