►
From YouTube: ROS 2 Security Working Group (14 Jun 2022)
Description
No description was provided for this meeting.
If this is YOUR meeting, an easy way to fix this is to add a description to your video, wherever mtngs.io found it (probably YouTube).
A
A
So
that
is
really
exciting.
To
hear
about
your
project.
There
could
be
a
lot
of
opportunities
for
synchrony
so
to
working
on
on
this
topic
as
well.
So
yeah
I'll
give
the
floor
to
you
feel
free
to
introduce
yourself
and
anything
anything
you
have
prepared
and
then
we'll
just
have
a
short
discussion.
I'm
just
open
to
two
questions
and
exchange
of
ideas.
B
B
My
my
expertise
is
not
not
so
much
in
in
security
is
more
on
safety,
but
be
that
as
it
may,
then
the
two
areas
are
actually
very
related
to
one
another
and
they
are
usually
both
desirable
traits,
especially
in
in
critical
systems
and
high
assurance
systems,
and
my
my
background
has
been
mostly
researching
this
topic.
Since
my
my
master's
thesis,
which
was
when
my
my
work
began
on
this
on
this
harvest
framework.
B
B
The
so
the
main,
the
main
ways
in
which
this
is
better
so
to
speak
than
using
the
the
known
techniques
directly
is
that
the
normally
these
techniques
are
already
a
high
barrier
to
entry
from
the
start
right.
They
they
require
already
complex
inputs
from
the
the
user,
like
formal
models
and
such
and
this
framework
instead
takes
source
code
directly
as
its
input.
So
it
works
directly
with
the
source
code,
which
is
the
the
language
that
the
the
average
user
is
used
to
to
to
use
in
everyday
activities.
B
And
then
we
do
some
some
reverse
engineering,
some
model
extraction
in
order
to
rebuild
the
the
formal
models
that
we
actually
need
from
this
code
and
then
specify
the
properties
that
we
want
to
verify
using
a
high-level
property
language.
That
is
more
or
less
like
a
script,
something
very
almost
english-like
that
people
can
easily
read.
B
Instead
of
writing,
greek
symbols
and
logic
formula
and
such
so.
To
put
this
in
perspective,
we
we
basically
start
with
the
user,
providing
an
input
file
and
that
we
called
in
the
contract
file.
This
file
basically
specifies
that
the
systems
that
you
want
to
analyze
and
the
properties
that
you
want
to
to
check
on
these
systems.
B
B
B
B
B
So,
instead,
we
treat
components
and
nodes
more
or
less
as
black
boxes,
on
top
of
a
common
middleware
which
is
lost
and
then
specify
the
behavior
in
terms
of
messages.
So
traces
of
messages
are
basically
the
observable
behavior
and
the
idea
is
to
use
a
higher
level
specification
language,
as
I
said,
that
is
backed
by
formal
semantics,
but
the
semantics
are
actually
even
away
from
from
the
user.
B
So,
basically,
a
property
has
two
components:
a
scope
and
a
pattern.
The
scope
defines
when
a
property
should
be
valid,
so
you
can
have
properties
that
are
always
active
so
to
speak
or
properties
that
are
only
valid
up
until
a
certain
point
or
after
a
certain
point,
for
example,
suppose
that
you
have
an
initialization
or
setup
phase
and
only
after
a
specific
trigger,
you
want
to
start
verifying
normal
behavior.
B
So,
for
example,
let's
say
that
we
want
to
to
specify
that
when
the
laser
detects
an
obstacle
closer
than
40
centimeters,
the
zero
velocity
message
is
published
in
in
response
within
the
following
500
milliseconds.
This
is
how
it
will
look
in
this
in
this
language.
This
property
is
global,
is
always
active
and
then
a
message
on
the
laser
with
a
distance
field,
less
than
40
causes
a
response
in
the
velocity
topic
with
the
the
linear
x
field
set
to
zero
within
the
500
milliseconds
afterwards,.
B
We
have
also
developed
by
me
and
the
two
plugins
one
for
runtime
verification
and
another
for
property-based
testing
and
property-based
testing.
If
you
don't
know
the
term
of
you
aren't
familiar
with,
it
is
basically
an
automatic
testing
technique
that
works
with
general
purpose
properties
more
or
less
like
we
have,
in
this
case
things
that
should
always
be
true
or
true
within
a
specific
context,
and
then
automatically
generates
more
or
less
randomly
a
large
number
of
inputs
and
repeatedly
tries
to
test
the
the
the
system
or
the
function
or
whatever.
B
You
are
testing,
with
this
generated
inputs
trying
to
to
break
the
property
first
and
then
trying
to
to
define
the
the
smallest
reasonable
counter
example
to
display
back
to
the
user.
So
this
is
more
or
less
that
the
workflow
of
this
property
based
test
plugin.
We
start
with
the
specification
or
the
the
properties
that
I
just
showed.
B
We
take
also
the
computation
graph,
which
is
automatically
extracted
from
the
source
code
and
the
message
definitions
for
each
type
of
message,
which
should
be
available
in
the
world's
installation
on
the
system.
The
plugin
puts
all
this
together
produces
a
test
script
that
then
automatically
generates
traces
of
messages,
enables
runtime
monitors
and
runs
a
testing
loop,
trying
to
find
contact
samples
for
the
given
properties.
B
In
the
end,
it
shows
reports
for
for
the
the
properties,
then,
that
fail
something
along
these
lines.
It
shows
which
property
failed
and
a
counter
example.
In
this
case,
the
counter
example
contains
only
one
message
with
a
distance
of
zero
on
the
topic
laser
at
that,
given
time
stamp
of
the
the
execution.
B
So
this
is
more
or
less
what
none
the
tool
is
capable
of
the
the
main
goal
of
this.
This
project,
this
framework
is
to
bridge
the
gap
between
robotics
and
software
engineering
or
developers
and
experts
in
formal
methods
and
software
engineering,
inc,
quality,
etc,
which
in
a
way
also
includes
security
and
should
include
security
as
well.
B
It
offers
a
variety
of
different
analysis
with
always
with
the
goal
of
requiring
as
little
user
input
as
possible
or
as
feasible,
and
the
system
and
property
specification
is
iterative
and
partial.
You
can
start
with
very
small
systems,
very
small
specifications
and
add
more
to
it,
as
as
you
go
in
terms
of
current
status,
this
has
already
been
tested
with
a
number
of
academic
and
industrial
case
studies
and
development
for
the
current
version,
which
only
works
with
goals.
B
One
is
suspended
because
I'm
currently
currently
basically
rebuilding
the
tool
from
scratch
to
work
with
ros
2
and
to
improve
a
number
of
things,
mostly
internal
systems,
trying
to
make
it
more
easily
accessible,
adding
more
more
hooks
for
for
plugins
different
points
and
maybe
not
only
for
analysis
and
such
so.
The
current
goals
is
basically
are
basically
to
to
rebuild
finish.
Rebuilding
this
tool
enable
ross
to
support
from
the
start,
maybe
take
this
opportunity
to
integrate
with
new
conventions
such
as
the
the
nodel
language,
to
specify
systems.
D
B
A
A
Yeah,
that
was
really
great,
and
I'm
really
happy
to
hear
actually
that
you're
working
on
rust
to
support
and
also
that
you
well
you're,
aware
of
nodel
and
you're
planning
to
integrate
and
take
a
financial
side
as
well.
That
is
one
project
that
people
from
this
working
group
have
contributed
to.
So
that's
that's
pretty
cool,
and
that
was
actually
one
of
my
questions
like
how
do
you
see
that
two,
for
example,
yeah
projects
like
no
deal
interacting
well
with
hros
and
benefiting
from
it.
B
C
Yeah,
I
will
say
you
know.
The
first
thing
that
I
was
going
to
ask
about
was
going
to
be
the
ross
versus
ross2
thing
I
was
over
here.
You
know
kind
of
searching
through
the
github
repository
just
to
confirm
my
suspicions
on
that.
So
yeah.
I'm
also
really
glad
to
hear
that
that's
moving
forward,
I'm
curious
about
you
know
the
way
that
you've
got
the
you
know
properties
set
up
to
define.
C
You
know
what
the
expected
behaviors
are
and
then
going
through,
and
you
know
trying
to
generate
counter
examples:
how
how
large
of
a
concept
can
that
really
you
know
contain
because
you
know
the
example
here
is
pretty
straightforward
of
okay.
If
I
see
this
thing
at
less
than
40,
then
I
should
therefore
expect
this
other
one
to
appear
with
a
zero,
but
I'm
kind
of
thinking
of
some
of
the
larger
scale
real
world
examples.
C
B
It
also
has
quite
a
number
of
features
that
that
enable
describing
more
complex
cases.
For
example,
you
have
this
junk
these
junctions
for
for
topics.
For
example,
if
you
hear
that
the
input
is
laser,
but
you
could
say
laser
or
bumper
or
whatever
wheel
sensor
or
something
along
those
lines,
you
can
have
a
number
of
different
messages
being
the
alternative
inputs
and
then
leading
to
also
possibly
different
responses
and
within
the
the
the
so
the
filters
for
for
the
messages
so
to
speak.
B
In
this
case,
the
conditions
are
pretty
simple:
it's
basically
distance
less
than
40
and
in
the
other
case,
it's
linear
x,
equal
to
0.
But
these
internal
patterns
for,
for
the
messages
are
also
quite
complex.
They
can
include
every
data
type
that
is
in
the
that
is
allowed
in
in
roth
messages,
and
you
can
even
have
sort
of
quantifiers
and
loops
over
the
the
fields.
If
you
want
to
traverse
arrays
or
describe
that,
for
example,
all
fields
in
an
array
must
be
less
than
some
threshold.
C
B
So
we
are
to
to
adjust
the
the
the
resulting
test
scripts
basically
to,
for
example,
select
from
a
data
bank
or
something
from
those
lines
instead
of
just
going
random,
because
most
of
the
time,
if
you
are
generating
images,
randomly
it's
going
to
just
be
noise
and
won't
make
any
sense.
So
you're
just
wasting
time.
D
D
Good,
could
you
it
a
little
it
escaped
me
a
little
bit,
but
could
you
go
back
to
the
section
where
you
discussed
the
transitive
flow
from
one
subscription
and
one
publication
to
the
other
in
terms
of
like
these
time
windows,
I
I
didn't
quite
catch.
Maybe
you
go
back
in
the
slides.
I
think
you
had
somewhere.
B
D
Specification
of
properties
and
causal
and
requirements
so
here
you're
discussing
about
the
required
outputs
and
the
required
inputs
and
checking
like
if
you
had
a
if
you
had
a
depth
camera
that
was
publishing,
point
clouds,
rgb
images
and
maybe
a
depth
map
or
something,
and
you
have
a
filter
that
needs
to
subscribe
to
all
those
three
to
generate
a
colorized
point
cloud.
Is
that
what
this
kind
of
scenario
would
encapsulate.
B
B
B
B
Yeah
I
I
can.
I
can
specify
deadlines
from
input
to
response
for,
for
example,
but
defining
that
that
response
is
dependent
on
multiple
synchronized
inputs
is
not
well
supported
right
now,
but
I
I
think
it's
not
impossible.
It's
just
a
matter
of
manpower
for
implementation
and
including
it
somehow
in
the
language.
So
in
some.
D
B
D
D
B
That's
something
that
is
probably
going
to
be
necessary
at
some
point,
especially
for
for
messages
that
have
a
lot
of
quantifiers
or
arithmetic
expressions.
Those
are
a
bit
harder
to
generate
automatically,
but
in
in
many
cases
I
can
evaluate
the
expressions
statically
and
basically
generate
code
that
always
produces
valid
messages
by
by
construction
and
for
some
some
educat
cases
or
other
patterns.
B
D
B
So
so,
basically
like
this,
this
simple
example
for,
for
example,
here
we
will
have
to
generate
as
input
traces
of
messages
that
include
at
least
one
laser
message,
because
otherwise
you
will
never
be
testing
the
this
input
and
response
pattern
right.
If
you
never
have
inputs
you,
you
will
never
get
on
the
test.
This
makes
sense.
B
So
that's
one
of
the
constraints.
The
the
input
trace
has
to
contain
at
least
one
laser
message,
and
in
this
case,
since
the
the
pattern
itself
is
very
simple,
it's
just
a
numeric
field
less
than
the
static
value,
then
I
can
basically
take
that
and
generate
code
that
always
produces
valid
inputs.
So
I
basically
take
this
condition
and
make
it
so.
The
the
random
generators
always
generate
values
that
are
less
than
40.
E
B
Everything
up
to
this
point
up
to
the
the
the
extraction
of
the
graph
is
just
looking
at
source
code.
Nothing
on
the
raw
system
has
to
run
for
up
to
this
point,
then,
for
the
remaining
of
the
analysis,
it
depends
on
the
plugins,
but
obviously
the
the
test
generator
will
have
to
execute
the
system
at
some
point
to
run
the
tests,
but
other
things
like
model
checking.
B
For
example,
only
workflow
models
doesn't
have
to
run
anything
as
well
as
possibly
other
simple
static
analysis
tools,
things
like
linters
and
things
like
cpp
check
and
such
that
detect
uninitialized
variables
in
code,
and
that
kind
of
thing
you
can
do
that.
Only
looking
at
the
code,
you
don't
have
to
to
run
anything
but
for
tests.
Obviously,
we'll
have
to
to
execute
the
system.
At
some
point.
B
Yeah,
the
the
specification
is
in
this
case
is
basically
that
the
properties
those
have
to
come
from
from
the
user.
It's
it's
in
this
input
file.
Basically,
you
have
here
at
the
bottom,
a
section
in
which
you
will
write
down
the
the
properties
or
some
link
to
an
input
file
that
provides
these
properties
and
but
yeah.
Obviously,
the
properties
are
always
to
come
from
the
user,
because
it's
the
user,
the
the
user,
is
ultimately
the
the
person
who
knows
what
should
be
valid
in
their
system.
E
B
Yeah,
that's
one
of
the
things
that
we
do
with
this
type
of
queries.
For
example,
one
we
have
some
that
that
run
automatically
the
the
user
won't
have
to
write
them,
and
one
of
them
is
trying
to
to
detect
topics
for
which
there
are,
for
example,
publishers
and
subscribers
using
different
types
of
messages,
maybe
because
they
badly
configured
remapping
or
something
that
ends
up
matching
topics
that
that
should
not
be
matching
and
that
can
be
automatically
detected
only
by
looking
at
the
source
code.
E
And
did
you
have
the
chance
to
run
some
robustness
examples
and
for
the
quotational
graph
creation,
since
the
question
came
from
one
of
the
work
that
we
did
very
often
on
discovering
the
the
graph
of
the
robotic
system?
If
this
is
not
a
simple
published
subscriber,
the
number
of
nodes
increases
exponentially.
E
B
B
E
All
right
and
one
last
question:
probably
what
about
the
functional
non-functional
requirements?
So
you
have
properties
that
you
can
express
for
the
robots
for
software
development
for
the
devops,
especially
when
you
want
to
prove
some
functional
functional
requirements
for
safety.
For
example,
you
mentioned
that's
one
of
the
fields
you've
been
exploring
and
working
on,
and
you
had
some
experience
in
developing
those
kind
of
solutions
as
well,
or
you
only
been
defined
properties
that
are
functional
in
this
case,
like
the
velocity
and
the
radar.
B
But
of
course,
then
there's
a
lot
more
to
non-functional
requirements
than
than
deadlines,
but
yeah.
My
my
main
focus
for
for
research
has
been
on
on
functional
safety,
so
that
that's
what
I
I
most
easily
support
up
until
this
point,
but
my
my
current
employer
for,
for
example,
has
a
serious
focus
on
on
security.
E
All
right,
thanks
and
really
the
last
one
question
some
of
the
folks
here
we
have
been
working
on
devsecops
for
robotic
systems
and
we're
waiting
for
the
review,
but
for
the
iros,
but
we
had
the
chance
to
discuss
about
it
here
in
the
in
the
working
group
chats
and
also
on
discord.
I
would
like
to
know
if
you
had
a
chance
to
check
that
out
and
if
it
might
be
on
of
your
visitors
for
you,
since
you
are
also
targeting
now
ross
2
and
security
as
well.
E
If
you,
if
you
have
seen
the
the
work
we
we
tried
to
push
about
the
cops,
I
think
it's
quite
interesting
for
your
research
as
well.
We
are
trying
to
to
to
reach
the
same
conclusion
so
now
that
we
are
also
pushing
for
the
roster.
I
was
just
wondering
if
you,
if
you
have
seen
that
and
if
you
have
some
ideas
or
some
comments
about
it,.
B
Yeah,
I'm
not
very
familiar
yet
because
I
I
just
despite
knowing
about
the
existence
of
ross
2
for
for
basically
it's
it's
launching
2017.
I
think
I've
only
recently
started
studying
it
learning
it
and
I'm
just
basically.
I
only
started
in
the
first
months
of
this
year
delving
into
what's
going
on
in
the
last
two
environments
what's
going
on
in
terms
of
software
quality
security
and
such
so
I'm
not
yet
familiar
with
a
lot
of
stuff.
A
B
E
E
B
Yeah
so
my
my
phd
ended
basically
july
of
the
the
last
year
and
since
then,
I've
been
working
at
this
vortex
laboratory
that
you
see
the
logo
at
the
bottom,
but
the
the
situation
is
more
or
less
than
the
same.
We
do
not
have
a
lot
of
manpower
yet
and
basically,
the
harvest
framework
has
been
my
solo
project
since
the
beginning.
D
D
I
can
send
it
send
it
also
there
in
a
chat,
so
you
can
have
a
look,
but
it's
this.
Basically,
this
big
ss11
implementation,
eprosmartdid
for
fast
dds.
Last
year,
we
worked
together
on
that
and
we
are
now
working
on
something
else
for
for
fast
dds
with
them,
and
this
came
up.
So
I
promise
to
pretty
much
ask
ask
around
if,
if
anybody
here
knows
how
to
how
to
kind
of
poke
this
forward.
D
The
this
seems
like
it's
on
the
rmw
repo,
so
the
client
library
working
group
might
be
via
the
go
to
folks,
with
the
permissions
at
least
to
merge
all
right.
Do
they
have
their
own
metrics
chat
or
or
what's
the
easiest
way
to
kind
of
raise
them
up.
So
under
the
rost
two
working
groups
on
the
ross2.org
index
or
whatever,
I
think
there
is
an
entry
for
the
calendar
schedule
for
the
client
library,
I'm
not
sure
if
they
have
a
instantaneous
chat,
but
they
do
regularly
meet.
A
A
Okay,
great,
so
thank
you
so
much
andre
for
a
great
presentation
for
your
time.
It's
been
amazing
here
about
aeros,
very
interesting
projects
and
great
discussion
as
well,
so
you're
very
welcome
to
join
us
anytime,
so
we're
holding
this
meeting
once
a
month.
It's
a
community
meeting
and
it's
always
announced
on
those
discourse.