Fundamentals

Formally Verified and Publicly Verifiable E-counting For Complex Voting Schemes

FeM Channel
Rajeev Gore
This is a talk about how we can generate single transferable votes counting code from a logical specification automatically using advanced computer aided verification methods. It is based upon a PhD dissertation but I think I made it non-technical.
I will first explain single transferable vote counting and the parlous state of computer-counting code implemented by various Election Commissions from around Australia. I will then explain how we used Coq to specify a "vanilla" version of single transferable voting as a proof-calculus and used it to extract a computer program which not only counts votes according to this specification but also produces a certificate during the count. The specification of the certificate is derived from the counting rules. We have proved, in Coq, that if the certificate is correct with respect to its specification, then the result it encapsulates must be correct with respect to the relevant specification of single transferable voting. The certificate is designed so that an average third-year computer science student could write a computer program to check the correctness of the certificate.

Additional information

Live Stream https://streaming.media.ccc.de/rc3/fem
Type Talk
Language English

More sessions

12/27/21
r3s - RemoteRheinRuhr Talk
Daniel Maslowski
r3s - Monheim/Rhein
With approaches dating back to the 20th century, the idea of a TPM is simple: An isolated, constrained environment to offload trust establishment in a larger computing environment. That implies cryptography, firmware, hardware, and per application, different requirements. This talk elaborates on how the seemingly simple concept has been expanded over the years, enumerating implementations in hardware, firmware, other layers of software, and even web browsers, explaining why it is in fact far ...
12/27/21
chaoszone crew
ChaosZone TV
Feierliche Eröffnung des ChaosZone TV Channels beim rC3 2021.
12/27/21
Thomas Fricke
c-base
In den letzten Wochen der scheidenden Bundesregierung erhielt der Sprecher eine Mail von der Open Knowledge Foundation https://okfn.de/en/ über seine Meinung zur Open Source Sicherheit. Daraufhin erstellte er er eine Studie zum Thema Sicherheit von Open Source Projekten. Vier Projekte dienten als Beispiele und deren Hauptakteur:innen wurden befragt. Darunter "the random programmer from Nebraska" https://www.explainxkcd.com/wiki/index.php/2347:_Dependency Ariadne Connill ...
12/27/21
r3s - RemoteRheinRuhr Talk
Siebo M. H. Janssen
r3s - Monheim/Rhein
kommt noch - wird nachgereicht - Wunschtermin: 27.12.2021 gegen Mittag - einzige Möglichkeit
12/27/21
Thomas Fricke
c-base
Tokens are a powerful way of controlling the access to to Rest APIs. Chasing them should be hard. Unfortunately, there is a widespread habit of leaving tokens lying around allowing very powerful attack vectors. An attack demonstrates how to hack an OpenShift cluster, which is fully securty compliant to the accepted standards of NIST and CIS. Hijacking a container gives full control to the cluster, including host access. If running in the cloud, the cluster can be used for further attacks, ...
12/27/21
Back to Basics
avocadoom
Chaos-West TV
Ein Einsteiger-Talk über statische Webseiten, wie man sie erstellt oder auf diese umstellt und dabei seinen bisherigen Workflow beibehält und welche Vor- und Nachteile diese mit sich bringen.
12/27/21
Chaosstudio Hamburg
Chaosstudio Hamburg
In diesem Talk stellt sich die 2020 gegründete Volksinitiative Hamburg Werbefrei vor, für alle die etwas gegen die zunehmende Vereinnahmung der Stadt durch Außenwerbung unternehmen möchten.