►
From YouTube: hacspec: succinct, executable, verifiable specifications for high-assurance cryptography
Description
Denis Merigoux, Franziskus Kiefer and Karthikeyan Bhargavan
A
A
So
choosing
grass,
as
you
all
know,
is
a
way
to
circumvent
that.
Hence
there
is
a
new
shiny,
rust
band
for
photography.
Libraries
with
names
such
as
transcriptor
bella,
cryptography
ring
raspy
for
post
quantum
cryptography,
but
also
whole
protocols
written
in
rest,
such
as
rastialis,
and
this
new
band
has
kind
of
distance
from
the
old
verified.
Gourd
of
cryptography
verified,
cryptography
libraries
with
projects
such
as
evercrypt
apple,
star
veil,
which
are
all
like,
bundled
in
the
same
thing,
but
also
fiat
crypto
from
the
mit
or
jasmine
crypt
from
the
equipment,
technique
and
other
institutions.
A
A
And,
as
you
have
been
able
to
see
in
this
workshop,
the
verification
tools
are
still
maturing.
Hopefully,
one
day
they
will
handle
the
full
functional
correctness,
proof
for
crypto
libraries
with
like
10
000
or
100
000
lines
of
code,
but
they
still
still
not
there.
So
we
have
to
find
something
in
the
meantime
and
our
approach
is
rather
focused
on
crypto
and
we
do
not
aim
to
become
like
a
general
purpose.
A
A
Of
course
those
won't
be
performance
oriented,
but
so
we
also
want
for
them
to
be
easily
to
have
the
possibility
to
easily
switch
to
a
native
rust,
like
hanse-fevi,
optimize
implementation
and
for
proof
people.
Well.
This
language
is
aimed
at
providing
the
proof
of
people
with
a
steady
source
of
correct
reviewed
by
domain
experts.
Specifications
that
they
they
can
they
take
to
as
a
basis
for
their
functional
correctness.
Proofs,
therefore
reducing
the
trusted
computing
base
for
proof
development.
A
A
Indeed,
since
we
wanted
this
dsl
to
have
simple
semantics,
which
mean
that
we
had
to
take
radical
decisions
in
order
to
cut
whole
branches
of
complex
rusty
medicines,
which
we
didn't
want
to
talk
about,
and
the
actual
trade-off
that
we
had
while
designing
this
language
is
on
the.
On
the
one
hand,
that
cryptographers
should
be
able
to
write
beautiful,
specs
like
succinct
and
that
don't
look
ugly
and
on
the
other
hand,
we
don't
want
to
too
much
features
in
language
in
order
to
avoid
the
semantics
creep,
which
will
lead
to
very
complex
formalizations.
A
And
I
know
some
people
in
the
audience
have
yet
dealt
with
all
that.
Those
semantics
complications
in
rust
and
we
didn't
want
to
go
through
that.
We
leave
that
to
experts
and
for
more
complicated
functions
like
this
main
poly
loop.
You
can
see
that
it's
all
about
like
for
calling
functions
with
some
kind
of
sequences,
so
we
have
like
slicing.
A
We
have
four
loops
that
are
indexed
by
integers
and
it's
generally
a
feeling
of
us.
We
have
also
mutable
variables,
which
are
then
translated
to
some
kind
of
state
monad
with
that
keep
like
the
variables
as
the
state
of
the
variable
as
the
the
states,
and
you
can
see
that
we
a
little
bit
of
boring
but
in
various
very
very
particular
places
it's
only
at
the
top
level
in
only
in
function.
A
A
We
have
two
kind
of
fixed
length
array,
one
which
is
like
whose
length
is
known
at
compile
time
and
the
other,
whose
name
is
not
known,
compile
time.
This
distinction
is
useful
because,
with
the
first
kind,
you
can
implement
the
copy
type,
which
is
very
useful
to
have
specs
look
nice
to
not
insert
blue
and
everywhere.
A
Concerning
statements,
we
have
fairly
limited.
It's
only
led
bindings
conditional
for
loops
and
also
array
updates
scenario,
indexing
and,
concerning
the
expression,
were
fairly
straightforward.
We
have
tuples,
we
currently
don't
have
structs
in
inner,
so
we're
planning
to
add
them
in
the
future,
and
we
have
also
array
indexing
and
all
of
the
usual
operator
on
the
integers.
A
We
provide
this
language
with
a
simple
call
by
value
symbolics
with
context
such
as
the
variables
the
local
variables
of
a
function,
so
values
are
like
usual
values,
plus
arrays
and
doubles,
and
the
shape
of
our
judgments
is
really
simple.
We
just
have
this
variable
context
and
the
expression
or
function
argument
or
statement
divides
to
a
certain
value
while
changing
the
variable
context.
A
All
the
rules
for
semantics
are
presented
in
the
paper.
I
you
should
go
and
read
the
technical
reports.
If
you
want
to
get
more
precision
about
that,
we
also
provide
a
typing
judgment
that
is
meant
to
respect
rust,
specificities
with
linear
typing.
So
we
have
a
typing
context
containing
both
tuple
functions
and
variables.
A
We
have
a
type
dictionary
to
provide
the
indirection
and
the
nominal
nature
of
rust,
struct
typing,
and
we
have
a
linear
context
splitting
to
implement
the
linear
nature
of
frost
type
system
which,
with
an
escape
hatch,
which
is
the
implementation
of
the
carby
traits,
we
don't
implement
traits,
we
don't
formalize
traits
in
our
language.
We
take
it
as
some
types
to
implement
them
and
some
of
them
don't
it's
part
of
the
context
and
we
have
a
simple
typing
judgments.
A
A
So
then,
because
we
want
to
offer
convenient
tooling
to
cryptographers,
we
had
to
implement
a
type
checker
and
basically
compiler
for
this
embedded
dsl
and
of
course
we
do
that
as
a
plug-in
to
the
ras
compiler.
But
then
and
we
we
took
an
unusual
choice
with
respect
to
the
other
tools
presented
in
workshop,
because
we
wanted
our
representation
to
be
very,
very
close
to
the
source
code
and,
as
you
guys
can,
as
you
know,
mir
is
very
distributed
and
is
in
basic
blocks
form.
And
so
I
know
they're
working
around
around.
A
And
so
let
me
show
you
a
little
architecture,
diagram
of
the
spectacular,
so
it's
in
implemented
as
a.
Why
not
use
hir.
This
is
a
good
good
question,
because
hrr
has
a
little
bit
of
syntactic
sugar
and
we
didn't
want
to
deal
with
that,
especially
with
respect
to
four
loops.
It
disregards
the
for
loop
into
a
while
loop,
I
think,
and
it
was
not
convenient
for
our
users,
so
we
took
asd
also
because
it
allows
us
to
control
more
easily
with
respect
to
what
we
get
in
the
source
group.
A
We
translate
it
into
a
hackspace
ksc
by
re
and
in
the
process
rejecting
all
the
programs
that
are
outside
the
bounds
of
the
dsl,
and
then
we
perform
the
hotspot
type
checking
and
we
can
also.
We
also
have
support
for
external
crates,
meaning
that
you
can
have.
You
can
split
your
programs
in
several
crates
and
we
integrated
compiler
architecture
that
lets
you
split
your
hack,
spec
programs
into
several
crates,
which
is
something
that
is
quite
painful
in
terms
of
engineering
but
which
we
thought
was
crucial.
A
And
this
was
very
important
because
we
want
to
the
specs
to
be
succinct
and
as
small
as
possible
because
they're
the
trusted
computed
base.
So
we
want
to
then
to
minimize
that-
and
here
is
what
the
the
outputs
in
a
verification,
backend
look
looks
like,
and
you
can
see
that
the
charge
align
function
which
I
was
showing
to
you
earlier.
A
But
the
output
of
our
tool
chain
is
relatively
similar
to
the
original
code,
and
we
want
that
because
then
proof
people
are
going
to
look
at
that
code
to
prove
functional
correctness
against
implementation.
So
we
were
seeing
sickness
and
pleasantness
to
read
is
definitely
something
that
we
look
for.
A
On
top
of
the
language,
we
have
several
libraries
that
provide
convenient
functions
that
cryptographers
always
use
in
the
recommendations.
We
have
a
great
for
secret
integers
that
are
just
wrappers
around
sine
and
unsigned
integers,
but
that
forbids
all
non-constant
time
operations.
You
can
also
use
that
crates
separately
from
the
hexpec
language.
Actually,
we
have
a
crate
for
abstract
integers
that
are
a
verification
freely
bound
in
natural
integers
and
because
they're
bounded,
we
can
fit
them
inside
an
array,
a
few
eighths
that
implements
the
copy
traits.
A
A
In
conclusion,
this
is
an
ongoing
research
collaboration
between
full
methods.
People
mostly
represented
by
inria,
with
my
phd
advisor
kartik
and
me,
but
also
with
many
cryptographers,
the
first
of
whom
being
a
franciscan
foreign,
but
we
also
are
talking
with
various
professors
that
are
leading
verified,
crypto
implementations,
research
teams
all
over
the
world.
A
So
there's
a
website
whose
link
is
on
the
screen.
The
code
is,
of
course,
available
online,
both
the
code
for
the
hackspec
programs
written
so
far,
and
the
code
of
the
compiler
in
type
checker,
and
there
is
a
technical
report,
so
you
can
refer
to
if
you
want
more
details
on
the
formalization
and
on
any
of
this.
B
A
Yes,
yes
thanks
yannick,
so
crypto
is
it's
kind
of
the
same
family
of
languages.
I
don't
have
a
precise
comparison
of
what
of
in
terms
of
what
features
are
missing
in
hack
spec
and
what
feature
are
in
a
in
crypto.
So,
yes
for
the
recording.
The
question
is:
how
do
you
compare
hacks
back
with
crypto?
Do
you
gain
in
exclusivity,
for
instance,
compared
to
fixed
styles
of
data
in
crypto,
so
my
understanding
is
that
crypto
is
heavily
screwed
toward
spitting
out
assembly.
Isn't
it.
C
A
Yes,
which
is
why
you
have
fixed
size
of
data,
so
high
spec
is
a
little
bit
expressive
because
it's
it's
mostly
aimed
at
spitting
out
or
camel,
let's
say
ml,
so
and
and
then
it's
it's
used
to
verify,
implementations
that
are
in
c.
So
there's
a
little
bit
more
flexibility
in
terms
of
exclusivity,
so,
for
instance,
our
sec.
You
can
pass
an
arbitrary
sized
buffer
as
input
your
encryption
encryption
function,
for
instance,.
C
I
could
say
a
little
bit
more
about
the
comparison
with
with
kryptol,
if
folks
would
be
interested
in
that.
So
I
think
the
biggest
difference
between
them
is
just
the
structure.
The
kryptol
is
a
a
purely
functional
language
and
uses
sort
of
functional
idioms
for
describing
programs,
whereas
a
hackspec,
you
know,
even
though
it
is
copying
things
around
uses,
a
you
know,
uses
rest
and
is
is
kind
of
more
imperatively,
structured
and
probably
more
familiar
to
to
a
lot
of
programmers.
C
But
it
does
mean
that
you
are
kind
of
constricted
when
you're
writing
a
program
to
be
sure
that
all
of
your
functions
correctly
preserve
the
sizes
that
are
described
in
the
types.
So
a
big
part
of
it
is
that
it's
got
a
type
system
that
that
tracks
the
size
of
everything,
and
so
it
is
fixed
for
any
particular
run
of
the
program,
but
not
necessarily
for
the
definition
of
a
particular
function.
A
Well:
okay,
thanks
for
the
precision,
so
ralph
asks.
What's
in
what
the
next
step
is:
wiring
up
some
automatic
river
for
roscoe,
with
xp
as
a
spec
language.
Well,
it's
it's
one
of
the
next
steps
involved.
So
I
I
started
this
project
with
the
goal
of
doing
some
razerification
in
the
in
the
spirit
of
pristi
or
cruzo
or
other
projects,
and
then
I
I
got
sidetracked
mainly
because
doing
grass
repetition
is
really
difficult
and
the
goal
of
this
project,
which
is
prosecco's
goal,
is
tracked
to
link
up
cryptography
and
formal
methods.