Dear viewer, these subtitles were generated by a machine via the service Trint and therefore are (very) buggy. If you are capable, please help us to create good quality subtitles: https://c3subtitles.de/talk/2095 Thanks!
Hello, and welcome back to the
functional.
Our next speaker will be Rajeev Cary.
Until last year, he was a professor at
the Australian National University, and
his talk will be about how the counting
of elections with complex voting schemes.
If that happens electronically and
and verifiably
after the talk, there will be a Q&A
session, a live session here
to ask questions, post them in
the eye, see and channel
a hashtag RC three
Dash fan in the rocket chat at
Hashtag FEMM and in the
videos and Twitter with the
hashtag. Are you three fam without
the dash?
If you're in the rotation for a shower,
give this animal that song on missed
in that play out and also
fun translated of F, a native
of translated tombstone or I'm content.
Then we're talking about that talent to
hunt and now enjoy the talk.
Hello, everybody.
My name is Rajeev.
I used to be a full professor at the
Australian National University and now
emeritus, and this
is joint work with Millard
Galli, who was a PhD student
with us until a couple of years ago
and patents and who is an associate
professor at the end.
You just
before I go ahead, all of the
stuff that I'm talking about, the code
and the verification and the proofs
are available here if you want
them.
Okay, so what
am I going to talk about?
I'm going to talk about a way
that we can.
Count.
Complex voting schemes,
for example, the single transferable
voting scheme by computer,
but in a way so that
the results are both formally
and publicly verifiable
by pretty much anybody.
Okay, so
this is the overview.
First of all, I'm going to talk a little
bit about what in doing verifiable into
and verify abilities in
electronic voting as it's known.
Then I'll explain what single
transferable voting is.
Then I'll explain the parlous
situation of computer counting in
Australia.
Then I'll explain a little bit about how
interactive theorem proving works and
then the work that we did in more detail.
Now there's a lot of stuff here.
And so I'm I need to
give a flavor of
everything rather than going
to the depth of the details.
So I hope you'll bear with me, and I'm
more than happy to answer any questions
you have in the chat session afterwards.
So let's get going.
So in electronic voting,
the gold standard is
known as end in
verifiability, and
the way that they achieve it
is by three
steps which sort of feed into
each other.
So the first one is called cast
as intended, and the idea
is that a voter should
be able to verify in some
way that the electronic ballot
that he or she is casting
is actually what they intended.
Right. So the idea here is to mimic
a paper ballot, you know, because
when you put a paper ballot in the box,
you know exactly what you're putting in
the box.
But when you do electronic
voting via some sort of computer
terminal, you don't necessarily
know what the computer is actually
casting on your behalf.
And so as intended is
to make sure that your
the electronic ballot really is what you
meant it to be.
And there are cryptographic ways to
achieve that.
Recorded as cost says
that you must be able to provide
public evidence that the ballot was not
tampered with in transit.
Right. So it's all great.
The electronic ballot is what you
intended, but if there's a man in the
middle attack, then the man in the middle
can change the ballot in transit.
And finally, there's the tally
was recorded.
So the idea is that a voter can verify
that the ballot was telling, right,
in other words, that the tallying
program didn't just throw the ballot
away.
Right now, these three things naturally
form, you know, a cascade
so that if you have cast as intended
and then recorded as cast and
tallied is recorded, you have
in verifiability and there
are, you know, publicly available
electronic voting systems that try
to guarantee these things.
Now, most of these
solutions for the first two
are cryptographic in some sense, you
know, some sort of hashing, some sort of
mixing. I won't go into the details
now, tally this record.
It is all well and good.
You know that you know that your vote was
tallied.
But what is the vote counting program
contains a bug.
So what you really want to know
is that it was tallied correctly,
and that's what we're trying to address
in this work here.
And the idea is called
software independence, and it goes
back to Ron reversed one of the
co-inventors of RSA.
So the idea is that a vote
counting program has to produce
a telling script, write some sort of
evidence of what it was doing.
And then what we do is
we try and guarantee that
if the tallying script is correct
with some notion of correctness,
then the result is correct with
the appropriate notion of correctness.
OK, so there are two notions of
correctness here. One is the correctness
of the telling script and the other is
the correctness of the count.
And what we do is we formally
tie them together with this
implication in line
in Idea two.
Right. So that's a formal implication
which has to hold in logic.
And then our claim is that it's trivial
to write a program to check the telling
script, and I'm hoping to demonstrate
that in the rest of my talk.
OK.
So the idea
is rather than.
Verifying that every
run of the vote counting program is
correct.
What we verify is that this
particular run of the vote counting
program is correct.
Right? The one that counted your ballots
or the one that counted this election.
And so this idea of this
one is correct will come up
through my slides a little bit.
OK, it's a new take on formal
verification.
All right.
So what do we mean by a voting scheme?
So the example that I
want to deal with is single transferable
voting. So it's basically a method for
sitting out, filling in and counting
paper ballots, right?
Yeah, of course. If you make it
electronic, you still have to have an
electronic voting scheme.
But now we're out of the
the scope of what we've done.
So we have a paper ballot
and for example, like this
one here, it says that, you know,
there are four candidates and I
vote Charlie one, Dave
to Alice, three, and I don't
really care about Bob now, depending
on the voting scheme, this can either be
a legal ballot or not.
So, for example, do you
have to fill out all the numbers?
So in some jurisdictions, this would
be an illegal ballot because I haven't
put a floor here.
But in other jurisdictions, this is
allowed
in in the Australian
capital territory in Canberra, where I
am. What we do is we also do
something called Robson rotation,
and the idea is that if you just
have a fixed order of the candidates,
then the donkey vote, right?
The voter that doesn't care.
We'll just go one two three four
vertically and that those donkey
votes will all go to Alice.
And unfortunately, we have a lot of
donkeys in Canberra, and so there are
lots of votes that are donkey votes.
So what they do is they
produce reordered versions
of these ballots in all the possible
permutations and distribute them
to the physical locations in equal
numbers.
So the idea is that, you know,
the donkeys get equally distributed
through all of the candidates.
The main thing that we need to do, of
course, in counting, is detect
when a quota is
when a candidate reaches a quota.
If someone doesn't reach a quota, then
detect who the weakest candidate is
because that's who we're going to
eliminate.
And how do we break ties?
And how do we transfer a vote and when to
stop counting?
So as you can see, this has got nothing
to do with the cyber security aspects
of electronic voting rights about formal
verification of an algorithm.
And I'm going to go into the details of
STV counting now
to explain why it's hard.
So these are all the details or the
technical terms that I might use,
and I'm just going to talk about
how we count the ballots
and refer to these things.
So I'm going to let you read this.
Just note here that the transfer
value of a ballot can be less than or
equal to one. That's the main thing that
I want to get across.
Okay, so here is here
is a pile of ballots and
what do we do? We do the following.
We tally all the highest prefer
preferences.
So what does that mean?
That means that we create a
pile of ballots for Charlie,
and this ballot goes into Charlie's pile
and that's it.
Then we take the next ballot of
the pile and put it into wherever the
one candidate is.
So at the end of that, what we're going
to get is we're going to get in this case
for piles, one for Alice, one
football, one for Charlie and one for
Dave, and every pile
in, every ballot in
Charlie's pile.
We'll have a one here and every
ballot in David's pile
will have a one here,
and every ballot in
Alice's pile will have a one here and
so on. So the idea is that we've counted
the first preferences.
Now, if anyone meets the quota, if
whatever we fixed the quota debate, then
they're elected, I'll explain how that's
done in the moment.
But if nobody's elected, then
we have to choose a weakest candidate
and eliminate that candidate.
And either way, whether
we elect a candidate or we eliminate
a candidate, we have to transfer their
ballots.
So let me explain what transfering means.
So suppose that in the first count,
Charlie is elected.
So what we want to do now is we want this
ballot to go into Dave's pile.
But typically we don't
let it go in today's pile with a full
value because Charlie is
this voter has already got his or
her preference. By having Charlie elected
and now allowing them to have
a full vote to elect Dave
is sort of giving them more power.
So the idea is that we attenuate
the value of this ballot in some way
and the ballot value becomes less than
one and explain more
in a moment.
Of course, if the number of candidates
that are remaining is
is less than
the number of seats that we need to
elect, then you can just elect everybody.
OK, so that's also done in
the ACTU where I live.
Let me go into the details a bit more,
so here's an example.
So we have four candidates A, B,
C and D, we have to run an election
where we have to elect two of them.
And here are the five ballots in the
election. So a one
b to d three.
Similarly, D one
C to see one
d two.
That's what these ballots represent.
Let's assume that there are no fractional
transfers for the moment, so we don't
attenuate the value just to keep things
simple.
And let's not do this autofill thing
right where we elect
all of the candidates if
there are less candidates than the seats.
It just keeps things simple, for my
example.
Now in Canberra,
what we use is something called a drip
quota named after a person,
and it's defined to be this.
It's the total number of ballots, which
is five divided by
the number of seats, plus one, which
is three.
And it's the floor function, right?
So it's the greatest integer that's less
than that plus one.
So what does that mean?
It's five.
Divided by three is one point something
the floor is one plus one is two.
So as soon as someone gets to
vote in this election,
they get elected.
So what am I going to do now?
I'm going to count all the first
preferences, so I'm going to go down here
and count all the first preferences.
So as you expect, we should get a three
for a A, one for D
and a one for C.
So here they are.
Right is a three four, eight
one four D and one for C.
Now what now what we have to do is see
whether anybody meets the quota.
Well, it does meet the quota,
right? He has three ballots
and the quota is two ballots.
So he actually has one ballot more than
the quota. So let's elect a.
Now what we have to do is decide
what are we going to do with a surplus?
So what was the surplus?
Well, the surplus is one because
I only needed two of these ballots
to get across the line, but
a has got three.
So the surplus is one.
We have to decide how to
transfer the surplus.
There are various ways which I'll come
back to a bit later, but
right now I just want to keep things
simple. What I'm going to do is I'm going
to say, Look, all these ballots are
identical.
So let's just delete two of them and
transfer the third.
So let's just delete the first two
and transfer the third.
So what's going to happen is this ballot
is now going to move from this pile
to BS pile.
So bees count should go up by one.
And that's exactly what happens.
Now we have a three way tie.
Nobody is elected because nobody
meets the quota, so we have to
eliminate the weakest candidate.
How are we going to choose the weakest
candidate? We're again, there are various
ways and it makes a difference.
But for simplicity, let's
just pretend that this ballot,
because it's transferred, is somehow
worth less than these ballots, which
are not transferred, right?
I'm just making something up.
But there are much better ways, of
course, right?
So what I'm going to do is
I'm going to now transfer.
I'm going to eliminate or
eliminate a sorry, I'm going
to eliminate B and transfer
the ballot, right?
So I've eliminated B
and transferred the ballot to D.
But D now gets two votes
right. So we had because one
day equals one, we eliminated B.
The vote went to D, so D's count
goes to two.
He means he or she meets the quota.
And so D's elected.
And that's it. That's the end of the
election because we were tasked with
electing two people.
We elected two people, we eliminated
B and C's just left hanging.
As well, neither elected
nor eliminated, but
the winners are Andy.
Okay, so
what I'd like to do now is tell you a
little bit about the sad state
of affairs of electronic vote
counting in Australia.
We don't have any official electronic
voting. As such, we have
booths spaced voting in the act.
But I just want to talk about vote
counting.
So at the highest level, we have
the Australian Election Commission, which
counts the federal elections,
the national elections and as
you can see here, the code is hidden.
It's proprietary.
It's not available for scrutiny
when a lawyer in Tasmania
put in a Freedom of Information request
that the code be published.
He was denied by the Australian
Electoral Commission on the grounds of
security and commercial in confidence.
He appealed the decision to something
called the Arbitration Commission,
and the Arbitration Commission
threw out the defense of security
because the code is just run in
house, right? It's not connected to the
internet in any way.
But they
maintained the commercial in confidence
argument and denied the Freedom
of Information request.
Now what you should be asking yourself is
why would the highest electronic
authority sorry, election authority
in Australia have commercial in
confidence reasons for keeping their code
secret?
And it's because they make roughly
$19 million a year
by running elections privately
for electing the directors of companies,
and they don't want to endanger that
business.
So what they're choosing to do is they're
choosing to deny the public
the right to see the code,
which is used to elect their
representatives in the national
government because they want to make a
profit on the side.
The Victorian Electoral Commission also
has some proprietary code.
Victoria is the state where Melbourne is
also has some proprietary code code.
As far as I know, it's available for
scrutiny. But as far as I know, nobody
has done any scrutiny.
The situation that I'm most familiar
with is the Australian Capital Territory,
where the code was developed by a company
called Software Improvements using C++.
It's been used four times since the 2001
election and up until
recently the counting code, not the
casting code, but the counting code was
available from the website.
But in the last election, which happened
in 2019, they decided to keep
that secret as well.
Of course, the full code is available
if you're willing to sign a
non-disclosure agreement, which says you
shall not publish until we give you
permission to publish.
But being, you know, good
academics, we're not willing to do that.
The other province that I know of
is the New South Wales Electoral
Commission. New South Wales is the
province where Sydney's so
they make on their or at least
a couple of years ago, online
on their website, you could get detailed
functional requirements.
There was a letter from
a legal expert at the Queensland
University of Technology to say that
he or she thinks that the
functional requirements meet
the legislation.
Then the code was certified
by a company called Beardless Soft, which
I'm assuming is an Indian company because
I know that Burleigh is a big company in
India as
passing old tests.
But when you look at their certificate,
the very first line says we
give no guarantees that the code does
what it's supposed to do.
We just check this, this, this and this.
And you know, it's all okay.
It's proprietary code.
When we ask for
the code, they denied us the code,
and it's not available for scrutiny.
Okay, so what?
How can we sort of abstract
the approaches because I want to try and
keep things in the abstract?
So the idea here is that let's
look at three aspects.
So let's look at the artifacts that
exist, the scrutiny
that we can place them under and
lacking the scrutiny.
Where is the trust, the blind trust that
we have to place?
So we have, you know, a 14
page document which outlines
what the Hair Clock Act is
in Austria, in Canberra for
how to count votes, according to single
transferable voting and
the Australia, the Australian Capital
Territory Electoral Commission and
software improvements.
The company have come up with these
functional specifications in UML.
They're not published, but presumably
I could get them if I was willing to sign
a non-disclosure agreement.
So here we have to trust so.
Are improvements in the election
commission, then software
improvements have produced the computer
code in C++.
They're not willing to publish the code
well. They used to publish the counting
code, but they're not even doing that
now. And so what we have to
do is we have to trust this auditing by
some company called B.M..
So in
Canberra, the company that
certified the code or audited, the code
is called BMP.
Now, why on earth should you trust this
PMPM company?
What do they do?
Well, VM is a company that actually
audits gaming machines,
so I'm assuming you have them
in Germany as well.
But we have these things which we call
one of them and it's, you know, these
machines that you put money into and they
tell you they roll the dice and tell you
whether you've won the jackpot or not.
Now in Australia, the legislation says
that they have to return
some percentage of their takings.
Eighty five per cent has to be returned
to the players.
So this company actually audits
gaming machines and certifies them
to be correct in the sense
of returning 85 per cent of their
takings. So at some stage they decided
that, well, if we ordered
gaming machines, why don't we audit
software as well?
And so they audit software
again. The very first
page of their certificate says We do
not give any guarantees that this
code actually counts the ballots
properly.
A New South Wales, I have a similar
approach. So again, legal texts that
have forty seven pages of specs, but
they're actually published.
There was a vendor we don't know who
produced a computer code.
The computer code is proprietary.
You can't look at it.
But now we have to trust this company
called MuleSoft.
And again, the very first pages.
We don't guarantee that the code does
what it was supposed to do.
Now what's the situation?
So over the past two years, we've found
many bugs in the system,
and some of my colleagues have recently
found bugs in the New South
Wales system. So I'd like to tell you a
little bit about the bugs.
So the very first bug that we found was a
simple four loop error.
You know, what you want is a full and
outermost full loop that says something
like, you know, for
I equals one to the number of candidates
do blah blah blah.
Now that had a slight bug in that, so
they either had n minus one or plus
one. I can't quite remember which, but
one of the these students who
now works for Google Zurich found
that the code
would run perfectly fine if there was an
even number of candidates, but would
just crash and burn if there was an odd
number of candidates.
I can't remember which way it would have
actually happened.
We found the bug three days
before these people were going to count
the Act 2001 election
live on television on
the day of the election.
They admitted the error.
They fixed it, but we got this nice
letter back from the Election Commission
saying thank you for notifying
us of the simple error.
It was easy to fix and everything's fine
now.
So we asked them, Well, if there was this
simple error, how do you know there are
not other errors?
And they said, No, no, no, we're sure
everything's fine.
Of course, a little bit later, one of my
colleagues all went to found another
bug.
That's this one. Here he had it.
There was an unknown initialized Boolean,
and different compilers could give
different results.
Another one of my colleagues, Jeremy
Dawson, rewrote
the implementation or
rewrote his own implementation using
a functional programing language.
And when we checked the results of the
2001 election, we found
that three ballots were going in a
slightly different way at a certain
point. And we tripped when we traced
it. What we found is that there was a
three way tie right for
the weakest candidate.
So in a real election, there was a three
way tie where there were three
candidates always equal number of
votes and one none of them who met
the quota. And one of them had to be
chosen as the weakest candidate.
Now the the legislation
says that when you're in the situation,
you've got a three way tie.
You go back and go
back to the previous rounds until
all candidates have an unequal number
of votes.
Now, Jeremy's a mathematician, so what he
said is what does that mean?
Well, all candidates have an
unequal number of votes means
no two candidates have
the same number of votes.
Right. So what this English text actually
means is that all the ballots
have to be counts have to be pairwise
distinct, right?
So they are equal.
We have to go back until this one is not
equal to this one. This one is not equal
to this one and this one is not equal
to this one pairwise distinct
but the way the index code.
Wasn't doing that, what it was doing is
going back until one of them was
different.
So we wrote to the election commissioner
and said, Look, we think we found a
problem. Your code doesn't meet
the legislation.
And he wrote, It's a very nice letter
saying, thank you very much.
But we've defined
the meaning of this English text to be
exactly what the code our current
code does.
Right? Well, we can't argue with that.
He was the election commissioner.
How bad were these things?
Well, for every bug, we could generate
a very small election, which we could
demonstrably show
gave the wrong result.
But I just said we have full confidence
in our code.
The University of Melbourne group found
a bug in the New South quote in
the New South Wales code recently,
which actually reduce the chances of
a candidate winning from 90 per cent to
10 per cent.
The first question you should be asking
is why are we talking about probabilities
here when we're talking about an
election? And this is worth
discussing.
So let me go back to here where
I had to transfer
one of these ballots.
Okay, so remember that
as being elected and he's got
a surplus of one, and I need to transfer
these one of these three ballots.
So what we did was we just transferred
one of them because they are all equal.
What New South Wales does is something
really clever.
They randomly select one
of these ballots to transfer
and transfer that randomly selected
ballot, which is all fine in this case
because they're all equal.
But if these things were different, then
we would basically be flipping a coin
to see who gets elected.
And more importantly, what it means
is that you can't rerun the count
because your random number generator may
do different things at the same position
in the second count.
So what did my colleagues do?
What they did is they ran the election
100 times, and what
they found is that one
particular candidate was winning in
ninety nine per cent of their runs.
But in the real election, there was
a bug and it reduced the chances
of that person winning to 10 per cent.
But the person couldn't challenge
the result because the
three month period for a legal challenge
had passed.
So, you know, this poor person
potentially lost the election because of
a bug, but she couldn't challenge.
Now I want to talk about a better way
of doing things.
So I'm switching now, right?
So this is the parlous state of
electronic voting counting in Australia.
I want to try and talk about how to do it
properly, but in order
to do it properly, we need something
called a form of verification.
And so what I want to do is tell you a
little bit about formal verification and
what that means.
So formal verification started in the 60s
with an eye during
right, so artificial intelligence
researchers were dreaming about
automating mathematics.
So the idea is that we can do
mathematics fully, automatically on a
computer, and you can read a really nice
paper by a guy called
one of the authors is
John Harrison, who is
an expert in this formal verification
area, and he currently works for
Amazon.
Why? Because they want to do formal
verification of their code eventually.
Of course, what they found is that, you
know, automating mathematics
is the ultimate.
That's just give me a second.
Automating mathematics is the ultimate
undesirable problem.
And so human
guidance was indispensable.
Right. So they tried for 10 years
and basically realized that we needed
to be interactive.
It couldn't be automatic.
Now the reasons why
you might want to automate mathematics
began to get more and more serious.
So the first example was the Apple
hack and proof of the full color theorem.
This is the famous theorem that says you
take any Mac in three days
of countries and you can color
it in for
it at most four colors
so that no two countries have the
same adjacent, no
two adjacent countries have the same
color.
So Apple and Hopkin came up with a proof
in 1976, and there were some
1500 lines of code.
And people are asking, Is the code
correct? And I said, Well, we think
it is what we do.
The best example that I know of is the
Pentium bug in 1994,
because it cost Intel half a half
a billion dollars.
So they then
started hiring people in formal
verification, and they had a team for
many years. And John Harrison actually
used to work for Intel for a number of
years before he moved to Amazon.
The next example is called the Kepler
conjecture.
This was approved by Thomas Hales
that the best way of stacking oranges
is the face centered cubic
way. It's the way that your average
greengrocer at your market
stacks them.
But there was no proof that this was the
most space efficient way of
stacking oranges.
He came up with a proof, but it had
200 pages of handwritten notes
or typed notes and a three gigabyte
computer disk of examples.
So again, the journal said,
Well, we're not sure about this, but
you know, we think it's OK.
So what's the idea of formal proof?
The idea of formal proof is that we use
computers to do logic
based checking of
proofs. So we enter the proof
into a computer using a specially
designed language and the computer checks
whether the proof is correct or not.
As you can see, this is a chicken or
egg problem, because how do you know that
the computer program is correct?
And that's what I want to talk a little
bit about now.
This is actually a very
well developed area of research.
And the current goal, there are many
proof assistance, but the current goal is
actually to make them more human
friendly. So let me talk a little bit
about
formal proof, and I'm going to do that
using an example.
So let's take the example
of odd and even numbers.
So what's the definition of an even
number? Well, it's a number
which can be divided by two.
So it can be written and is even
if it can be written as two times some
other number right to, for example,
zero times zero
one times to two times
to three times to.
And so on.
What's an odd number?
Well, an odd number is just an even
number +1 write.
The odd numbers are sitting
in here, so it's zero plus
one two plus one four plus
one, five plus one and so on.
So now I want to prove a lemma.
If the natural number N is even,
then the natural number in +1 is
odd. So how can I do that?
Well, here's a simple proof.
How does it proceed?
So what we do is we say, OK, let's assume
that n is even that means
that there's some K
such that N is equal to two times
K.
So we know that this holds for our
even number N.
Well, now what we'll do is just will add
one to this and one to this.
And what will we get?
We'll get that in. Plus one is of the
form two times K plus one.
But what do we know about numbers
of the form two times code plus one?
Well, there are by definition,
so in plus one must be order.
All right.
Now what I want to do next is to
show you an example of a
computer script where a computer
program called Coque, which
is a theorem Prouver, an automated
proof assistant, has proven
this has checked the proof.
OK, so this is what it looks like
now. I can't go into the details, of
course, but the idea is this
that we import some library called
arithmetic because they've defined a
library, which allows us to do
arithmetic.
We define that
for the natural number N
is even if what?
Well, if there is a K sextet N
equals two times K, the
natural number N is odd.
If what exists a K sex that
N equals two times K plus one.
And here is a.
Encoding of dilemma for all natural
numbers in, if any, even
then in plus one is odd.
And this is the proof.
Again, I can't go into the details, but
these are commands that I've given
to the interactive zero prove.
These are comments where I've tried to
capture what line of the previous
proof I'm capturing here.
And the idea is that when I get down to
here, I type QED
and the computer program
is checking all these steps and it says,
yes, all the steps are correct.
Or it says no.
This step is wrong here.
Fix it up.
And so the idea is that we interactively
push the proof through Congress
through the details.
Okay, next question
you should be asking is why should we
trust machine check proof?
So what we do is machine check
proof is based on the Alonzo
Church's lambda calculus from the 1930s.
It's a published paper.
It's been reviewed for the last.
Goodness knows almost 90 years or so
by mathematicians.
The official
research laboratory in rail from
France has produced this COC the
improvement, which is about 50000 lines
of code. It's been in development since
1976.
It's been checked by lots of people
and everything is published.
And so yes, we do have to trust some of
these things.
But you can you can
actually check these things.
So the idea is that we're going to use
this framework to do
formally verified electronic
counting.
So here's a map of what we've done.
So what we did is we took
the legal text that's the English
for the pages of the Hare Clerk Act.
We manually transferred it into logic
as rules capturing the state
transitions of an automaton.
Right. So basically, the state
transitions where a computer moves
from this state to that state.
And we tried to keep the computer as
simple as possible.
Right. So we're not trying to mimic a
full computer.
We're trying to mimic some sort of
abstract machine capturing abstract
machine and logic.
Then we converted this legal text into
formulae of higher order into mystic
logic as our third functional
specification.
So this is logic and this is logic.
And what we proved in Cork is
that if this thing produces
a correct certificate with some
notion of correctness, then this
thing produces a correct count
with your partner notion of
correct count.
Again, I can't go into the details, but
I'll try to give you an example in a
minute.
Now these are the
cocking interactive zero gravity a so
well-developed that actually
we were able to extract the code
automatically, which I can't go into,
right? So the idea is that once you do a
proof in Cork and Cork accepts
the proof, you can generate the code
automatically. So we didn't write any
code, we just did a proof
and we press the button.
Why should you trust any of this, well,
everything's published right, you
can get your election expert to check
this. You can get your mathematical
logician from you, dodge that, say
to check this.
And the only thing you really need to
trust is the certificate, which
we're going to publish and you can check.
So that's what I want to go into now.
So what have we done?
We've completed STV vote counting
and also the Shultz's method.
The Shultz's method is used, for example,
by the Linux community when they
want to decide which way to
fork branches, our code
computes with extract fractions.
It's efficient. We can count up to 10
million votes with 40 candidates and 20
focuses in 20 minutes.
It produces a certificate.
It produces a paper
printout of the state machine
and what states it's going through.
And what we claim is that an average
third year computer science student can
write a program to check the certificate.
And that's what I want to go into
in a moment.
In in in reality, you don't even need
to trust the hardware, the software,
because all you need to do is check
whether the certificate is correct
because our proof guarantees you
that a correct certificate implies a
correct count.
Right. And the converse of this is that
incorrect count means incorrect
certificate.
So if you check the certificate, you can
check with the count.
So this is what I want to talk about now.
So what we actually did is we
encoded a minimal abstract machine,
which has three types of stakes.
There's an initial state where all the
ballots are uncounted.
There's a final state
where we declare winners.
And then there are a bunch of
intermediate states.
I can't go into the details, but the idea
is that these intermediate states
carry complicated data, which
are usually lists and ballots
are moving from one place to another
list, according to the state.
Transitions of this machine
and the state transitions correspond to
counting, eliminating, transferring,
electing and declaring winners as rules.
And so, you know, the machine moves
from this state to this state.
If you count, it moves from this state
to this state. If you eliminate
and that's captured in logic,
then what we did is we we actually
prove minimal conditions that
the rules need to satisfy for everything
to be correct.
Now I can't go into the details of this,
but what I want to do is give a simple
example.
So let's go back to that idea of the
actual numbers and what what I'll
do is I'll show you some coding,
which which includes the natural
numbers in the clock.
So this is actual copy code.
And it says to the clock theorem prove
that Capital Zero is my
type of natural number.
I'm defining my private type of natural
capital.
Capital is a my.
These are my type of natural number and
s is a function which takes
any natural nut mine that you give it
and gives back another natural number.
So what does that mean?
It means that zero is capital
O.
One is s of capital.
Two is s of S of capital,
so three is SL, s0
s of capital and so on.
So every natural number is represented as
a string, which ends
in capital O and has a number
of S's in front of it.
So what we did is the state
machine is encoded using this complicated
thing, and what you can see here is right
that there is this
initial list of ballots.
There is the final list of candidates
which are elected
and then there is a complicated structure
which captures these lists.
Again, I can't go into the details.
The minimal STV instance is then given
by the definitions of these rules
and the rules that satisfy the
respective conditions.
The conditions consist of two parts.
When is the rule applicable and how
does it change the state?
And then we in COC, we prove the three
theorems.
Every applicable transition reduces
complexity.
So whenever you do something, you're
reducing the complexity of what remains.
That means that eventually we have to
reduce the complexity to zero.
There's a notion called liveness, which
says from any state, you
can't be blocked.
There's always at least one exit,
right? And these do two things together
imply that whenever you give me a
set of ballots, my process will
terminate, right?
So I guarantee you that this is an
algorithm which terminates.
Okay, then what we did is we
use the code extraction for facilities
of got to actually extract the code,
which I can't go into.
And what we did
is produced a program that
actually produces a certificate
once the certificate.
It's a run of the state machine.
And what we claim is that it's easy to
write a program to check the certificate.
Again, I can't go into the details, but
I'll give you an example.
So going back to our
natural numbers, I claim that
this is a certificate of
correct edition,
right? So what is it?
It's just a stack of lines
of the form and something.
Something something.
OK. And in the same way,
this is a certificate produced
by our vote counting program.
And as you can see, it's a bunch of
lists. So this is a ballot which says
a preferred oversee, preferred
of a b, and it moves in some
way through the lists until we declare
a winner.
I can't go into the details, but
this is what's going on.
So the claim is that
to check the certificate, all you need to
do is simple pattern matching
and check that these actually are the
rules that are being used to go
from here to here, where these are the
rules at zero.
And that is in this
case, right. But in our case, it would be
to stop and count rules.
So now I want to go into
an example.
So keeping the example simple.
So what are we going to do is we're going
to define the natural numbers, as I said,
and we're going to say that a basic
derivation is any string of this
form that is a string
that starts with the word add
and has three things after it, all
of which are X, Y and Z.
But the first one has to be equal
to the third one.
And the middle one has to be bigger.
And why is that?
Well, because that just says that
adding zero to X is X,
and we know that adding zero leaves
x alone.
And then the step case is if
you know that adding extra y gives Z,
then you know that adding X to
Y plus one gives Z Plus
one.
And so all we're doing is we're inserting
s twice into this position
in this position to convert that to an
air supply and convert that to an s
of Z.
Right. So what's the derivation?
It's a stack of correct derivations
and the result is in the bottom.
And the theorem says a correct derivation
always contains a correct result.
How can you verify that?
Well, I claim that this is a correct
derivation.
So let's check, is this a correct
derivation? Yes, because
it's something and the same
thing with a big go in the middle.
That was a correct definition, and it
says that zero plus one equals
one.
This one is a correct definition, because
if this is a correct derivation, then all
we've done is added an s here and edit
it here, and this thing says
you can transform one correct derivation
into another correct derivation.
So this is a correct derivation.
What's the result?
One plus one is two.
And so what's the final result?
One plus three is four.
So all you need to do is you only need to
check are those rules that I took
that I specified up here.
And it's just a pattern matching problem.
So what? What's the election process?
So what we do is we publish our logical
encoding of the vote counting process.
We publish the specification of what
correct certificate means.
We published a mathematical proof
that a correct certificate implies a
correct result.
What does the software vendor do, the
software vendor to lose the program,
which is almost certainly buggy
for vote counting, but it has to produce
a correct certificate, it has to produce
a certificate according to what we mean
to be a certificate.
And what we mean to be a correct
certificate.
Now, of course, if the program is buggy,
it may not do that.
So the election authorities have to
publish all the ballots.
Now what can we do?
Well, now we can have very, very
widely available
scrutiny because look, the political
parties can each hire a third year
computer science student to write a
certificate checker.
What's a certificate check program?
They just look at what a correct
certificate means and what a certificate
means and encode
what it means for the certificate to be
correct, it's pattern matching.
Other academics could set a software
engineering project to sign a certificate
checker. So what we could have is
we could have lots and lots of
certificate checkers which have been
independently developed,
and it's highly unlikely that
all of them will contain the same
right? So what do we do?
Well, you run the election,
everybody checks and someone sets.
The public certificate is incorrect.
So what we say, OK, you claim that
the public certificate is incorrect.
Where does it break the correctness
criteria?
All right. We told you what it meant to
be correct.
You tell us where it's incorrect.
And if you tell us that it's incorrect in
line five thirty five.
So I know it's incorrect in going
from here to here.
Well, we can check that right.
So there's public checking of
that claim.
Then someone else says on your
mathematical proof is wrong.
So we'll say, All right, you claim the
mathematical proof is wrong.
Tell us where it breaks the rules of
logic. We've published our rules
and we published our proof.
So you could go to the people in Berlin
or Darmstadt or Karlsruhe
and get the academics there to check out
proofs.
Someone else might say the correctness
criteria or the mathematical mathematical
encoding is wrong.
Again, we say, All right, when you claim
something is wrong, give us an example
of where it does something wrong and we
can check. So the electoral experts can
check.
Finally, what if the vote counting
program is buggy or hacked,
right? We don't care,
because the theorem says
that the correct certificate implies the
correct result.
So the control positive says
incorrect result implies incorrect
certificate.
And we've got all these thousands of
people around Germany checking
the certificate.
Right. So what it says is that
the bug or even the hack
could not have manifested itself during
this run of the program.
Right. The hacker tried to do something
or the vendor had a bug in
their program, but that bug did
not manifest itself during this run.
So this one is correct.
That's the idea.
So what are we done?
We've completed STV counting, as
I said, we've completed that, Schultz
admitted.
Counts 10 million votes, blah
blah blah, right?
Certificate is a plaintext
certificate which vouched
for the correctness of the count.
And you don't even need to trust the
hardware or software because there are
all these certificate checkers written by
independent people
who will check the certificate.
Now, the only caveat the dangerous one
is that we have to publish your ballots.
And that's actually a problem because
what is known is that if you publish
ballots, then the election can be
vulnerable to something called a Sicilian
attack, which I won't go into for now.
What we've actually done is get
Millard has even verified
the certificate checker, so he has
produced us a verified
certificate checker, which is formally
correct with respect to the semantics of
C using a different theorem,
prouver interactive theorem or cake
eml we've had we can cover
all STV schemes used in Australia.
And the problem that we're really
interested in now is can we do
this to encrypted ballots
because that would remove this as
an attack.
So the message that I want to try and get
across to you in Germany is
verified and publicly verified
e counting is now possible.
Thank you for your attention.
Hello and welcome back and thank you for
the nice talk and someone in the chat
mentioned after hearing
a for the like
before hearing of Steve for the first
time, they thought the German electoral
system was complicated.
As a reminder, we have a Q&A session
now. If you want to ask questions, you
can ask in the IOC at 83
three minus them and the rockets at at
them and in the Twitter feed.
Diverse at eighty three.
And now welcome
to the Q&A session.
Rajeev should join us now.
Yes, he is here.
Hello and welcome.
Hi.
OK, we actually do have quite quite
a few questions. I'm positively surprised
about that.
And the first one is,
are there similar movements to public
money public vote in Australia?
And if that if
there is any international cooperation
between these movements?
And how do you do this?
Play into arguing against closed source
voting court.
So, so the first one is
about international
cooperation.
And as far as I know, there isn't any,
the only cooperation there is is between
academics like myself.
So there are groups in culture
where there are groups in France,
in India and there are various other
groups around the world that are trying
to push the election commissions
to take up our technology.
The biggest problem that we have is that
the election commissions
are not sophisticated.
Acquire, sorry, are not acquirers
of sophisticated software.
Right, so they're not like Nessa or
they're not like, you know, the space
commissions, they go
out to tender.
And you know, if a vendor says our code
is correct, then they just say, Well,
OK, yeah, the code is correct.
The vendor says so right.
And what was the second question?
Sorry, the how was
I going to argue?
How did this play into arguing against
closed source voting code?
So I think it was more about the push
to get the public to get
the voting code and the counting
code published.
Right. So so what's going on here
is it's a strange
confluence of interests.
So the election commissions
have built up a lot of trust over
the last 100 years, and the last
thing they want is to have their trust
undermined.
So what they don't want is I
don't want academics like jumping
up and down, saying there's a bug in your
code, there's another bug in your code.
And so what they prefer is to
say, our vendor guarantees us
that everything is fine.
Trust us, and
this is only going to change
when there actually is a disaster
and somebody's a losing
candidate challenges the result and it
goes to court.
And you know, the case is thrown out
and they have to run the election again,
and it's going to cost them in a couple
of million dollars and be very
embarrassing.
So the only time this will change
is when there's a disaster,
unfortunately.
And what we found around the world is
there are many academics like myself
jumping up and down saying, Look, we need
to do formal verification, and almost
all of them have been ignored by the
election commissions for the reasons that
I just explained.
Well, that sounds like the concept of
security, but security is still popular,
and so. Absolutely.
Absolutely. Yup.
Trust us.
OK, then maybe we get to the next
question regarding the Bucks in the
counting modules, whether any
requirements on the code quality to avoid
common mistakes, for example, by forcing
compiler warnings to be treated as errors
or using static analyzes.
I don't know.
They won't tell us.
All they tell us is that we've tested
the code extensively and it passes all
our tests.
Now you have to understand where the
election is coming from us here.
So in the old days, they used to count
ballots by hand.
Right now in Canberra, we have about
350000 voters.
And so, you know, they needed
to count these votes quickly by hand to
to declare the election.
And what happened is that in 1996,
there was actually a challenge and
it went down to some very small number
of votes, you know, three votes or
something like that.
And so Candidate A was declared the
winner candidate be challenged.
So they had to do a recount by hand,
which took a week.
Then the result went the other way.
Candidate B was the winner by five
votes, a challenge and Candidate
H challenged.
So then they had to do another recount,
which took another week.
And in the end, I can't remember the
result. But you know, it took three or
four weeks to
give the results the final results, which
were challenge free.
And so at that time, the Act electoral
commissioner said, Look, this is silly.
There's gotta be a better way.
Let's do it by computer counting.
But of course, what he or she doesn't
realize is that by doing it,
by computer counting, you're putting
all your eggs in one basket.
So you have a single point of failure
and you're putting a lot of trust on that
single point of failure.
And that's what we're not able to get
across to them.
OK, thank you.
OK, the next one is, have you proved
the cook to Husker compiler to be
correct? And are you certain that you
don't end up with the force as prediction
with force as a precondition anyway?
Right.
So this is the classic thing of
formal verification, which is garbage in,
garbage out. Right?
So if our formulas are inconsistent,
then we can prove anything we like.
And no, there is no proof
that coke is consistent.
There could well be some sort of serious
logical error. You know, in our
formal coding.
But.
At the end of the day, we have a proof
that a correct certificate implies
a correct count, right, which
you can check.
So even though
there may be a problem in clock,
we can tell you that that
bug in court didn't manifest itself
in our proof. If our proof is correct
and you can check the proof.
Right, so this is classic peer review,
scientific peer review.
You know, string theory might be wrong,
but it passes all the tests that we can
throw it at the moment because it
passes all the experiments that we can
do.
Yes.
OK. So I think the next question is
not completely serious,
it is does anyone trust a third year
computer science student?
Well, frankly, I would entrust
the third year computer science for the
Australian University, but I know
that in Germany, you teach them
properly and, you know, affordable over
their diplomas is not trivial.
So I trust Chairman Fuji computer
science students.
OK, I guess a lot of us would be happy
about that answer.
OK, the
next one is to what degree do voters
trust these voting machines?
And I'm not sure if if there were any
voting machines in the truck, but I guess
you have a better qualified to answer it.
Right. So in Canberra,
as I said, we don't have any electronic
voting, you know, by your
by your tap tablet or something
like that, right? What we have is you go
into a booth and the booth has
a computer with a screen and
you prepare, you know, you press the
buttons.
I think it's a touch screen.
You press the, you know, you touch the
screen to create your ballot and then you
say, you know, yes, this is the
ballot that I want to submit.
And then you get a nice friendly
screen that says, thank you very much.
Your your ballot has been cast
and you know, trust us right
now. What people should
be asking is, how do you know
that the ballot that you show
on the screen is the one that
you're actually casting?
How do you know that the machine isn't
making a mistake and casting, you know,
vote one Raj every
time?
And unfortunately, the
average voter is
not sophisticated enough to
ask these sorts of questions.
And so what they do is they say, Well,
you know, I can't check a pen and paper
election.
Who do I trust?
I trust the election authority.
And in this case, I do the same.
I don't know enough about
computer computers to know
that what's on the screen is what's
being cast, but I trust
the Election Commission to have done
their job.
OK. Yeah.
So another one
wants to know, how can you
clarify if you can clarify
whether and how you distinguish e
counting from e-voting?
Right. So if you remember, right
at the beginning, I gave you this idea
of end to end verifiable
voting.
Right, do you remember there was this
cascade? There was cast,
there was there was cast
as intended, there was
collected as cast and
counted as collected.
So the idea of electronic
voting is that you have all of these,
right? So you know, you cast your
ballot on your tablet.
Somehow, the tablet has
to give you evidence that
what you created on the
tablet was actually the electronic ballot
that was cast.
Then, you know, the the tablet
sends the ballot somehow
magically over the internet to
the election authority, and the election
authority has to produce some evidence
that you can verify that the
electronic ballot wasn't tampered with in
transit. And finally,
when the election authority publishes a
result, they have to provide some
evidence, publicly verifiable evidence
that you can
check to say that your ballot was
actually in the count right now.
So that's the traditional way of doing
electronic voting.
There are systems out there that do that.
As I said in Canberra, we have booth
based voting.
So you cast your ballot inside
a booth in privacy on a computer
that they say works properly.
Then the ballot is
somehow transferred to the election of
authority, which they say is secure and
everything is fine.
They count the ballots according to their
computer program, which they won't show
us, and they assure us that everything
is fine. So as you can see in Canberra,
we have nothing.
We have no end to end verifiability
because we have to trust the Election
Commission or the vendor at every stage.
Does that answer the question?
I guess so, so basically, you're
tackling this third of the three problems
without leaving the US to
out of scope.
Yeah, OK.
So another and there are cryptographic,
they're equipped.
There are incredibly intricate
cryptographic methods to solve the first
two.
And, OK, so another
one was in Germany, we have more,
more bizarre voting methods than a single
transferable votes and the idea of
if this would work with cumulative voting
or pan sorry, French
pan check or
it's red panacea.
Yes, I kind of think so.
Yeah. So in other words, is it a solution
for all situations?
The simple answer is, I don't know.
I haven't tried.
But as I said, my colleagues in culture
there's a there's a theoretical computer
science group and a verification, a
formal message group in Cultura.
They would be the people to understand
the German system.
I'm sorry, I just haven't.
I just haven't had a look.
OK.
But I have a I have a reverse question.
You said that the German system
is a bit bizarre, but I mean,
counting itself is pretty arcane as well,
right? So does it get any more
bizarre than STV
in Germany?
That's a good question.
I haven't looked into into the federal
election system lately, but it didn't
look so complicated to me.
But it could be in the local elections
that there are more complicated voting
systems.
But that's just my unqualified answer,
so that's probably a lot more,
lot more qualified people.
So so what's known is that Steve
is actually one of the hottest.
Okay, so there's an area called social
choice theory where, you know, people
typically mathematicians compare
different voting schemes.
And, you know, people have come
up with many other alternatives to STV
to try and make it fairer or better.
You know, there are at least 10 different
voting schemes that we could discuss.
But Steve is known to be one of the more
arcane ones because, you know,
everything depends on, for example,
how do you break ties?
How do you decide
who's the weakest candidate and this sort
of stuff? And for example,
in the
act system, the one in Canberra,
there's actually a clause which says if
everything is equal all the way up to
the beginning, then the election
commissioner can toss a coin, or he or
she could choose names out of a hat.
Right. So that's how, you know,
bizarre it gets.
Yeah.
OK, so someone noted that apparently
these more bizarre voting systems appear
in Bavaria like this one of the southern
states of Germany?
Yeah, actually, I knew that Bavaria was a
bit unusual. Yeah, yeah,
sure. OK, so the last of the
official questions, how is this
Typekit generated?
And the Oscar noted
that he or she might have missed it to
the during the talk.
The certificate is just a naive printout
of the run of the state machine.
Right, so I mean,
strictly speaking, you
know, we could be cheating,
what we could be doing is taking your
ballots and randomly generating
a certificate and claiming that
this certificate, correct, contains a
correct count. We might not even be
running a program.
Right? Literally, we could have
a thousand monkeys sitting on
typewriters, randomly generating
a certificate and then after,
I don't know, say an hour, we say
this is the certificate.
Right? And Raj wins.
But it doesn't matter because
the proof says that if you
can verify that the certificate
is correct, then the count
that it contains is correct.
So it doesn't matter if we generate it
using a random number generator.
I mean, we don't, of course, but strictly
speaking, we could.
OK, thank you. And one last question that
we had in the studio here.
And could you maybe elaborate a little
bit more about what was the problem with
publishing the vote?
You said there was this Sicilian attack,
but yeah, sure.
OK.
All right. So this goes back
to the mafia in Sicily,
and that's why it's called the Sicilian
attack. Right.
So what you want is, you know,
you're running, you have an election for
mayor and you want to make sure that Raj
gets elected because Raj is crooked and
you can bribe him and, you know, do what?
Get him to do whatever you want.
So what you do is you tell
the voter that I want you to
vote in a particularly arcane
way. Right.
So you vote Frederick
three and free to
one. And Raj, 17,
and you know, you're five
or something like that.
And then what you do is if you publish
the ballots, you can check whether
that ballot exists.
You know, is there a ballot that what was
it, three to 17 year old, five, Raj,
17, and Fred, one.
Whatever it was, if that ballot
is missing, then you know that
the voter didn't do as you asked.
And then you can, you know, either
burn down their house or, you know,
shoot their children or whatever you've
done to coerce them, right?
And so in
Australia, in STV,
it's actually very plausible because,
for example, you know, we have elections
where there are 43 candidates
and you can encode your ballot
in many, many different combinations
to be unique.
And so, you know, we ask you to
vote in this way.
And once the ballots are published, we
check whether that particular
perversely generated ballot
is in there.
And what we've done, of course, is made
sure that we're scattering all the
candidates except the one that we want to
win and making them win.
Does that help?
Yes. For me, it makes it makes it
understandable, it basically breaks the
basic assumption that any vote you would
like and the way you vote is really
actually secret.
That's right. So you can uniquely
identify a vote because of the complexity
of the system.
Yes.
OK.
Let me ask the tough questions.
Perfect. Thank you so much.
Rush for four for your talk
and also for for the very detailed
answers. And thank
you very much.
OK.
And now on the film channel,
the next.
The last thing for today happening is the
Herrod news show at midnight and
tomorrow it's continues.
Or we continue at 5:00 p.m.
with writing lecture notes directly in
Ludeke and then see you.
Bye bye.