►
Description
We will show some preliminary results of our ongoing work to enable formal specification and verification of HLF chaincode. The proposed methodology consists in using the tool Why3 [1] (and its underneath language WhyML, and third-party SMT solvers) to specify, implement and prove the chaincodes. The tool Why3 then extracts an OCaml chaincode. Finally, we developped OCaml-chaincode-shim [2] to make OCaml chaincodes executable by an HLF peer. We will demonstrate the application of this methodology on a no code development scenario of a workflow supervisor (that could be a critical component of an industrial supply chain traceability system). This scenario starts with an abstract specification of the workflow in a graphical formalism (in the vein of [3]) and ends with a formally verified chaincode living in a HLF testnet.
[1] : Filliâtre, J. C., & Paskevich, A. (2013, March). Why3—where programs meet provers. In European symposium on programming (pp. 125-128). Springer, Berlin, Heidelberg.
[2] : https://github.com/hyperledger-labs/fabric-chaincode-ocaml
[3] : Bistarelli, S., Faloci, F., & Mori, P. (2021, November). *. chain: automatic coding of smart contracts and user interfaces for supply chains. In 2021 Third International Conference on Blockchain Computing and Applications (BCCA) (pp. 164-171). IEEE.
----
Hyperledger – Open Source Blockchain Technologies
Hyperledger is an open source community focused on developing a suite of stable frameworks, tools and libraries for enterprise-grade blockchain deployments.
It serves as a neutral home for various distributed ledger frameworks including Hyperledger Besu, Fabric, Sawtooth, Indy, as well as tools like Hyperledger Avalon, Cactus and libraries like Hyperledger Aries, Ursa. Learn more about Hyperledger projects: https://www.hyperledger.org/use
Discord: https://discord.gg/rVCn4j7UFd
Case Studies: https://www.hyperledger.org/learn/case-studies
Training & Certification: https://www.hyperledger.org/learn/training
Tutorials: https://www.hyperledger.org/use/tutorials
Webinars: https://www.hyperledger.org/learn/webinars
Events: https://www.hyperledger.org/events
Vendor Directory: https://www.hyperledger.org/use/vendor-directory
Subscribe to the Hyperledger Newsletter: https://www.hyperledger.org/newsletter
Follow-us on Twitter @Hyperledger
Learn about Hyperledger Membership: https://www.hyperledger.org/about/join
#Hyperledger #Blockchain
License
Creative Commons Attribution license (reuse allowed)
A
A
A
B
C
This
torque,
okay,
it's
working,
this
torque
is
divided
in
two
parts.
In
the
first
one,
I
will
start
by
describing
you
the
framework
of
our
work
I.
Will
you
will
hear
about
the
use
of
hyperledger
fabric
chain
code
in
the
nuclear
sector,
along
with
the
application
of
for
formal
methods
regarding
those
chain
codes?
C
I
will
then,
give
you
an
overview
of
the
different
steps
composing
of
our
generation
of
formally
verified
hypo
laser
fabric
chain
code
that
suits
our
needs
in
in
the
second
part
of
this
talk.
Francois
will
present
you
his
work
on
the
implementation
of
a
shim
with
the
okmul
language
that
we
use
to
make
our
general
generated
chain
codes,
work
on
hyperledger
fabric,
but
first
a
little
bit
of
context.
C
The
research
and
development
department
of
odf
identified
the
need
to
manage
and
Trace
convincing
data
from
industrial
operations
of
the
nuclear
industry
in
a
more
secured
and
transparent
way.
There,
therefore,
they
are
thinking
about
decentralized,
Ledger,
technology-based
business
process
management
management
system
to
control
and
track
the
course
of
those
industrial
Opera
procedures,
which
makes
it
a
critical
system.
In
several
regards,
it
is
used
to
classify
the
criticality
of
a
system
into
four
categories.
C
In
the
case
of
our
system,
a
failure
or
an
erroneous
Behavior
would
not
threaten
anyone's
life
and
would
not
cause
a
stop
to
death
operational
activities.
However,
a
system
failure
could
harm
the
company
image
and
the
trust
its
partners
and
customers
placing
it
or
result
in
a
lick
of
sensitive
information.
C
C
We
can
justify
the
use
of
hyperledger
fabric
blockchain
by
listing
the
main
advantages
it
provides
to
our
system.
Thanks
to
fabric,
we
have
a
permission,
blockchain
technology
that
enables
us
to
control
the
participants.
We
also
have
Smart
contracts
or
chain
code
confidentiality
and
private
data
collection
to
secure
sensitive
data.
C
C
The
user.
Formal
methods
is
a
suitable
response
to
this
necessity
of
guarantees,
because
mayor
testing
is
not
enough
as
it
never
fully
tests
a
program,
but
thanks
to
formal
methods,
we
can
obtain
guarantees
of
Correction
at
different
levels
and
degrees.
First,
we
can
use
a
strongly
typed
programming
language.
C
We
can
prevent
runtime
errors
at
the
pro
of
the
program,
such
as
division
by
zero
and
overflows.
We
can
also
certify
functional
properties,
properties,
sorry
over
the
code,
with
suitable
tools
and,
lastly,
we
can
carry
out
a
formally
verified
program
generation,
which
is
the
method
providing
the
most
guarantees.
C
It
leads
us
to
our
contribution
and
positioning
in
a
previous
hyperledger
fabric,
webinar
shim
developed
in
the
Haskell
programming
language
has
been
presented.
This
language
relies
on
a
strongly
typed
system
which
enables
to
implement
change
codes
in
a
safe
typing
environment
and
thus
strengthens
the
trust
in
the
code.
C
So
at
this
stage
we
want
to
specify
the
execution
order
that
must
be
enforced
between
the
tasks
and,
in
other
words,
enforce
the
workflow.
It
is
sometimes
a
strict
order
with
sequential
sequential
tasks
following
each
other
and
sometimes
a
looser
order
where
tasks
can
be
performed,
commutatively,
which
is
represented
with
the
dotted
boxes.
C
C
C
A
C
So
first
is
a
color
for
paper
performed
by
the
editor,
which
enables
a
submission
of
an
article.
Then
the
first
reviewer
purchased
a
favorable
view,
but
not
the
second
one
which
leads
to
another
submission,
after
that,
both
reviewers
separately
agree
on
the
new
version
of
the
article,
which
enables
the
journal
to
publish
it
and,
finally,
to
close
this
call
for
paper
procedure.
Instance.
C
As
you
can
see,
this
formalism
includes
a
notion
of
Rendezvous
represented
by
the
plus
symbol
and
the
notion,
sorry
here
and
a
notion
of
interruption
with
the
minus
symbol
which
takes
precedence
over
the
execution
of
the
tasks
running
Inside.
The
Box
foreign
then
comes
the
code
generation
from
the
constraints
expressed
with
the
graphical
specification.
C
This
very
kind
of
properties
could
be
useful
to
test
the
workflow
specification
and
convince
the
user
that
the
graphical
phase
was
performed
well
and
proving
those
properties
could
be
achieved
with
model
checking,
as
it
has
already
been
explored
on
solidity.
Smart
contracts
adopted
for
business
processes
as
the
general
generated
code
is
only
a.
C
Chain
code
derived
from
a
graphical
ordering
constraints,
it
is
easy
to
fill
each
method
with
a
code
implementing
the
business
application
of
each
task
at
the
yml
level
and
to
provide
a
specification
of
it
to
prove
its
correctness.
This
way,
we
can
enhance
the
chain
code
by
tracing
specific
data
while
leveraging
the
Y3
proving
environment.
C
A
C
Are
abstracted
they
are
declared
and
specified,
but
not
implemented,
which
means
that
we
have
to
provide
to
the
extraction
tool
the
way
to
call
the
function.
Gate
set
input
state,
for
example,
in
the
okml
environment,
and
we
can
thus
extract
executable
code
from
the
yml
implementation
of
the
chain
code
and
I
will
now
let
Francois
talk
about
his
work
on
a
shim
implemented
in
the
okml
programming
language.
D
So
the
shim
is
an
important
part
of
the
aperizer
fabric.
It
is
communicating
with
the
under
sir,
which
execute
the
chain
code,
and
each
found
also
are
connected
to
the
order
of
Imperial
public.
So
the
interesting
part
about
the
pressure
fabric
is
that
you
can
in
fact
use
many
different
language,
because
the
other
third
just
run
a
Docker
virtual
machine
and
connect
to
a
program
using
the
grpc
communication
protocol,
and
so
the
program
needs
a
little
bar.
D
Currently
we
are
only
the
gym,
you
know
camel
only
work
in
a
development
mode,
so
the
development
mode
allows
someone
to
directly
connect
to
the
endorser
the
program
directly
connect
to
the
endorser,
and
so
it
allowed
people
to
restart,
modify
and
restart
the
chain
code
at
wheel,
and
the
reason
is
just
that.
Currently,
we
have
not
explained
to
the
end
of
the
or
to
start
a
Docker
instance,
but
we
should
be
able
to
do
that
in
the
future.
D
D
So
we
take
the
protobers
reporters
that
describes
these
protocol
fabric
protocol.
Then
it
generates
the
fabric
protocol
or
camel
code,
and
from
this
description
and
grpc
product
plugin,
that
is
able
to
run
the
protocol,
then
we
can
have
fabric
chain
called
shim.
That
is
really
the
shim
that
the
user
can
use.
D
We
can
see
here
a
little
example
or
you'll
an
L
World
example.
So
at
first
we
open
this
module,
so
it
has
a
for
a
new
camera
code
and
then
the
two
for
the
function
query
and
put
are
the
methods
that
are
going
to
be
the
method
of
the
chain
code.
They
are
very
simple
here.
The
only
thing
they
do
is
to
get
the
key,
the
value
of
a
key
or
the
put
method
modifies
the
value
of
a
key.
D
D
So
we
you
can
see
that
here
it's
really
beautiful
applied,
because
we
just
recover
from
the
message
the
function
name
and
the
argument.
Then
we
match
from
the
function
name
in
order
to
know
which
method
to
call
and
with
that
you
can
communicate
from
our
Command
code,
you
can
create
a
we
have
this
chain
code.
Inocument
can
see
a
little
demonstration.
So
so
it's
really
so
what
we
do
here.
We
have
a
legal
script
that
will
create
and
compile
all
the
under
the
under
the
order.
D
It's
a
little
longer
I
speed
up
the
the
video,
and
so
at
the
end
we
will.
We
have
the
gear
chain
code,
invoke
Commander
available
and
so
in
the
other
terminal.
I
can
start
the
camera
code
using
during
the
build
it
and
started
it
automatically,
and
then
we
can
ask
the
value
of
a
the
key
n.
So
we
have
the
answer.
90..
D
D
So
in
the
this
work
have
been
simplified,
a
lot
thanks
to
the
ascal
shim,
because
we
have
been
able
to
look
at
their
work
and
how
that
work,
because
sometimes
because
the
documentation,
in
fact
the
real
implementation,
is
a
very
good
explanation
of
what
hoshima
should
do.
The
portable
description
simplified
a
lot,
the
work
too,
and
yet
the
protograph
is
not
completely
explicit
and
for
some
message,
it's
hard
to
know
where
to
find
each
important
part
and
to
know
which
data
is
available
for
the
different
messages.
D
C
Yeah,
so
we
presented
you
the
different
steps
carrying
carrying
out
our
family,
verified
apologia
fabric
chain
code
generation,
implementing
procedures
and,
in
our
use
case,
industrial
procedures
in
the
nuclear
sector.
We
also
presented
you
a
shim,
implemented
it
with
the
occament
programming
language
that
we
use
for
to
to
make
work
our
generated
chain
codes
and
for
future
future
work.
D
D
Often
it
is
a
very
small
piece
of
code,
but
that
are
quite
important
because
since
you
are
putting
in
them
in
those
blockchain
in
order
so
that
other
people
can
look
at
them,
P
other
people
have
to
trust
them,
and
also
you
yourself
need
to
be
sure
that
nobody
will
use
it
in
a
way
that
you
don't
want
to,
or
you
haven't
expected
and
so
proof
allows
to
show
to
yourself
and
to
your
others.
The
behavior
of
the
problem
then
also
to
remove
a
usual
programming
error
like
a
rise
overflows
and
things.
D
D
D
So
this
question
is
about
that
in
an
approval
for
each
organization,
but
can
each
organization
have
a
different
chain
code
I
think
it's
possible,
but
really
I'm,
not
a
neurologist
expert,
so
I
think
I
have
seen
a
thing
like
that
where
people
have
different
chain
code,
but
it
must
be
for
different
things.
The
context
of
different
chain
code
for
the
same
feature
for
the
same
thing.
D
Oh,
and
so
whatever
and
answer
for
the
question
that
yes,
it
is
aesthetically
possible
as
long
as
they
produce
read,
write
sets
that
match
at
the
end.
So
yes,
that's
another
Stinger
feature
that,
yes,
it's
just
that
if
origin
of
sir
have
the
same
computation,
then
yes,
they
agree,
and
so
it
works.
Indeed.
Nice
so
perhaps
will
copy
paste.
The
GitHub
link.
A
D
D
And
so
it
is
not
directly
completely
a
tutorial
for
eBay
Ledger
in
the
way
that
we
are
not
using
apella
API,
it's
more
something
that
is
akin
to
solidity
API,
but
I
hope
it
will
still
be
interesting
because
it
will
show
you
what
we
want
to
prove
what
properties
we
can
prove.
All
the
proof
is
done
and
another
aspect
of
Y3
that
you
can.
You
have
a.
D
So
the
if
we
go
back
to
the
tutorial
in
this
ignitive,
so
the
goal
is
to
just
prove
a
transfer
smart
contract.
We
just
want.
We
have
a
better
the
balance
of
each
for
each
address
to
each
user
and
we
want
to
code
a
function
to
transfer
token
from
one
to
the
other.
So
it's
really
the
first
chain
code
you
can
height.
Someone
will
want
to
write
a
very
simple
one,
but
we
are
going
to
see
that,
in
fact,
there
is
a
many
pitfalls
that
the
the
set
pulls
help
avoid.
D
D
All
these
parts
fabric
is
already
written,
for
example,
Julia,
and
so
here
it
we,
you
have
it
just
in
order
to
have
a
Standalone
file
and
at
the
bottom
here
we
have
all
smart
contact,
the
code
that
we
want
to
pull.
So
this
code
can
be
compiled
to
solidity,
to
caml,
to
kkml
to
many
other
language
and
now
also
a
going
through
to
a
camel
yeah.
D
So
this
is
so
we
have
this
transfer
function.
I
people
is
what
it
does
is
just
so
it
takes
from
the
message
we
have
the
sender.
We
have
the
number
of
tokens
that
is
given
as
argument.
The
receiver
also
is
given
as
argument,
and
we
want
to
move
to
remove
this
number
of
tokens
from
the
sender
and
add
them
to
the
receiver
and
I.
D
D
D
We
don't
want
that
because
we
we
it's
not
the
semantic
we
have
in
mind,
and
so
we
don't
want
something
that
is
unexpected.
So
we,
the
semantic
we
choose,
is
that
here
it
is
an
error
and
it
is
a
the
we
ask
this
when
we
have
a
this
kind
of
computation
that
the
computation
will
not
be
below
the
row.
We
not
return
so
and
in
fact
we
can
see
here
that
it's
asked
the
computation
to
be
inside
the
bond.
D
D
Solidity,
where
which
is
to
abort
the
the
computation,
if
something
is
not
verified,
so
here
are
copy
pasted
the
line
that
will
explain
what
it
does.
We
add
this
require,
so
it's
a
function.
The
test
is
a
number
of
token.
Is
it
requires
that
the
number
of
token
is
smaller
than
the
balance
of
the
sender?
D
A
D
The
or
the
exceptions
that
can
appear
inside
the
code
must
be
listed
and
at
first
it
can
be
thought
as
something
that
is
quite
just
a
copy
paste
of
what
we
have
below.
But
in
fact,
we'll
see
that
it's
quite
interesting
for
multiple
reasons.
The
first
one
is
that
if
you
have
a
very
big
code
in
fact
inside
those
multiple
color
function,
call
you
can
have
other
require.
That
will
also
stop
the
computation
and
the.
D
A
D
D
Mathematical
integers,
and
so
here
we
can
ask
to
do
the
verification,
and
this
one
is
verified.
The
exception
of
this
post
condition
is
also
checking
that
it's
indeed
on
in
this
case
that
the
required
field
is
raised,
but
we
still
have
another
one,
because
indeed,
in
fact,
there
is
not
only
the
fact
that
someone
doesn't
have
enough
token,
which
is
what
we
think
at
first.
You
must
not
give
more
than
what
you
have,
but
the
problem
since
we
have
finite
integer
that
you
can
have
too
much
token.
D
Because
if
the
the
receiver
have
a
lot
of
token-
and
here
it's
really
a
lot,
because
it's
a
256
byte
longer
integers,
but
it
can
be
a
problem,
and
here
we
can
find
it
and
we'll
see
something
interesting
here.
What
we
want
to
say
is
that,
if
we
have,
the
number
of
token
of
what
we
want
to
write
is
something
like
that
that,
if
I
take
the
maximum,
the
the
max
of
wind
to
another
56
I
want
the
number
of
token
plus
the
balance
to
be
smaller
than
this.
D
D
D
A
D
D
D
D
D
D
D
It
is
I'm
saying
here:
when
are
the
the
required
failed?
It's
when
it
is
bigger
than
the
okay,
so
here
everything
is
proved
so
I
know
that
when
I'm
going
to
execute
this
function,
no
the
the
integer
knowing
computation
will
wrap
around
and
I
know
that
the
method
will
fail
only
in
those
two
cases-
foreign.
D
So
now
we
can
go
beyond
that
now.
We
have
just
something
that
will
be
executed
in
a
safe
way,
but
we
are
not
sure
that
we
are
Computing
it.
The
behavior
of
the
function
is
the
one
we
want,
because
what
we
really
want,
for
example,
one
property
that
we
are
interested
in
is
to,
for
example,
be
sure
that
we
are
not
creating
a
token,
because,
if
I
removed
this
line,
everything
will
be
will
work.
D
We,
it
will
be
food
also,
but
in
fact
I'm
creating
token
and
that's
something
that
I
don't
want
and
also,
for
example,
the
GAO
attack.
It
is
a
well-known
attack,
all
the
now
attack
on
etm
and
someone
have
been
able
to
to
to
together
a
lot
of
money
from
a
smart
contract,
because
it
was
a
removing.
It
was
not
removing
the
money.
The
balance
was
not
correct,
and
so
it's
what
we
are
going
to
try
to
prove
now
we're
going
to
prove
the
appropriate,
the
property
that.
D
D
Express,
what
the
sum
of
balance
is
and
other
sum
of
the
mapping
is,
and
so
we
are
going
to
say
that
the
sum
of
the
balances
is
always
equal
to
initial,
so
we
have
a
number
of
initial
token
and
at
any
point
we
have
always
this
number
of
targets.
Well,
so
it's
not
at
any
point.
In
fact,
during
the
execution
of
a
function,
we
allow
the
invariant
to
be
broken.
D
It
allows
us
to
to
to
do,
for
example,
this
computation
here,
where
we
remove
some
token
at
some
point
that
we
added
later
so
in
the
middle.
The
number
of
the
invariant
is
broken,
but
he,
but
at
the
end
it
will
be
restored,
and
so
what
I
wrote
is
that
here
we
have
the
in
Number
the
invariant
that
the
sun
balance
is
equal
to
the
initial
value
number
of
the
term,
and
this
by
is
to
ensure
that
the
environment
is
verified,
at
least
by
one
pair
of
balance
and
an
initial
value.
D
A
A
D
Just
yeah
in
the
tutorial
I
asked
to
add
this
function,
I
hope,
but
here
it
was
a
missing
from
the
definition
of
a
mapping.
So
now
we
are
so
it's
a
typing,
and
now
we
have
so,
for
example,
here's
invariant.
We
prove
that
the
type
is
habited
and
that
it
is
possible
to
verify
the
that
the
invariant
for
some
value
and.