Call for Papers: Unsound - Sources of Unsoundness in Verification (Deadline Extension: 2022-09-16)

7 views
Skip to first unread message

Jan Bessai

unread,
Sep 2, 2022, 4:43:21 PM9/2/22
to Jan_Bessai, marco.s...@vuw.ac.nz, coq-...@inria.fr, idris...@googlegroups.com, fscd.co...@dcc.fc.up.pt, types-a...@lists.seas.upenn.edu, ecoop...@ecoop.org, isabell...@cl.cam.ac.uk, jmlspecs...@lists.sourceforge.net, why3...@groupes.renater.fr, cedill...@googlegroups.com, it-fmeurope-e...@lists.uu.se, it-fmeuro...@lists.uu.se
==================================================================
Call for Papers

Unsound:
1st Workshop on Sources of Unsoundness in Verification
at SPLASH 2022
https://2022.splashcon.org/home/unsound-2022

Software and proof verification has grown significantly in the last 15
years.
Growth has come to the point where verification systems are complex and
manually proving the soundness of those verification systems sometimes
exceeds what a single research group can understand and verify as
correct.

Even formally defining soundness can be challenging and its definition
is varying from system to system. Specific research groups can have very
specific notions of soundness they focus on, but those can diverge from
what the users expect, especially if the users come from a different
verification environment or they are approaching verification for the
first time.

Participants to Unsound will be able to share their experience and
exploits on how different verification tools can either be broken or
expose confusing behavior, likely to be unexpected by users.
We think this would be greatly beneficial not only because it will help
all of us to iron out those unsoundnesses but also because it will
facilitate understanding of the foundational differences between the
assumptions of the various research lines.

The current academic environment encourages us to talk about the success
case of our work. In this workshop we want to address and learn from
failure cases and we want to reinforce the bedrock of our understanding.
In practice, when we divert our focus to a specific aspect of
verification
we may (understandably) be less precise.
For example, a line of research focusing on aliasing control in OO may
be less precise when considering the implication in other areas, like
termination.
We believe that learning from the issues of many verification projects
can broaden the attention of researchers to topics which so far escaped
their focused area of research; e.g., from only type correctness to also
avoiding stack overflows.

We believe that this environment would be particularly beneficial for
young researchers that are in search of open questions in verification.
This may provide a motivation to deep dive into the details of any
particular tool, or to expand their individual area of expertise to get
a wider and more objective and critical view of the whole area of
verification.

We also wonder if in our fast expansion we accidentally glossed over
some fundamental issue in verification, and if our mistake has now
become engraved into the established wisdom and it is sometimes
uncritically assumed as a valid reasoning stepping stone.

We are particularly interested in sources of unsoundness that are
accidentally shared by many different unrelated research lines, and to
develop an understanding on why this is the case.

The workshop would be its first instance and is meant to be welcoming
for both people with strong theoretical skills, as well as people who
just like hacking things. We do not expect fully polished submissions
and we will not have formal proceedings. Students are especially welcome
to attend.


### Examples for possible contributions would be:

* Definition of sound and unsound and how they can diverge between
tools.
* Divergences between user assumptions and actual definitions of
soundness.
* Common sources of unsoundness and why they emerge.
* Bugs and unsoundnesses in the process of extracting a concrete program
from a verified environment, e.g., from Coq to Haskell.
* Logic errors in the specification of a verification tool, e.g.,
universe
inconsistencies.
* Bugs in the implementation of proof checkers.
* Overconfident generalizations of sound subsystems to larger settings,
e.g., imperative techniques in OO settings.
* Disproving soundness statements in published papers about
verification.
* Finding statements proven in published literature that should no
longer be trusted because they relied on a broken verification system.
* Simply proving False in a verification tool, in particular we are
interested in practical ways to trick available tools to accept wrong
statements.
* Breaking reasoning about programs with types by breaking the type
system of the programming language in new and interesting ways.
* Bad interactions between axiomatic choices in libraries used in
proofs.
* Impacts of the false sense of security when the chain of trust is
broken by
subtle unsoundness in verification tools.


### Contributions:

*Extended Deadline: 2022-09-16 (23:59 AOE)*
Submissions should have 3 pages of text. Additional material
(bibliography, related work, and code examples) will not count toward
this limit.
We strongly encourage authors to include instructions to reproduce
results or exploits.

There will be a friendly peer review process, focusing on checking that
the submitted material is appropriate for the workshop.

#### Publication
Informal proceedings will be made publicly available on the workshop web
page. However, presentation at Unsound does not count as prior
publication, and can later be published at a conference of the authors'
choosing.

### Instruction to Authors

#### Submission

Authors should be aware of ACM’s policies on plagiarism
(https://www.acm.org/publications/policies/plagiarism).

Program Committee members are allowed to submit papers.

Papers must be submitted online at:
https://unsound2022.hotcrp.com/

#### Formatting:

Submitted papers should be in portable document format (PDF), formatted
using the ACM SIGPLAN style guidelines. Authors should use the acmart
format, with the acmsmall sub-format for ACM proceedings. For details,
see:

http://www.sigplan.org/Resources/Author/#acmart-format

It is recommended to use the review option when submitting a paper; this
option enables line numbers for easy reference in reviews.
Reply all
Reply to author
Forward
0 new messages