[TYPES/announce] CFP: LangSec 2021 (affiliated with IEEE S) due on Jan 15th, 2021

[Gang (Gary) Tan]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]


Call for Papers
7th Workshop on Language-Theoretic Security (LangSec)
Affiliated with 42nd IEEE Symposium on Security and Privacy (Oakland)
May 27th, 2021

The Language-Theoretic Security (LangSec) workshop solicits
contributions of research papers, work-in-progress reports, and panels
related to the growing area of language-theoretic security.

Submission Guidelines: see http://langsec.org/spw21/

Submission link: https://easychair.org/conferences/?conf=langsec2021

Important Dates:
Research paper submissions due: January 15 2021, AOE
Work-in-progress reports and panels submissions due:
  February 1 2021, AOE
Notification to authors: February 15 2021
Camera ready: March 5 2021

Topics: LangSec posits that the only path to trustworthy computer
software that takes untrusted inputs is treating all valid or expected
inputs as a formal language, and the respective input-handling routine
as a parser for that language. The parsing must be feasible, and the
parser must match the language in required computation power and
convert the input for the consumption of subsequent computation. The
7th installation of the workshop will continue the tradition and
further focus on research that apply the language-theoretic
perspective to policy mechanisms, such as treating policy formulation
and enforcement as language definition and language recognition
problems. The following is a non-exhaustive list of topics that are of
relevance to LangSec:

* formalization of vulnerabilities and exploits in terms of language
  theory
* inference of formal language specifications of data from samples
* generation of secure parsers from formal language specifications
* complexity hierarchy of verifying parser implementations
* science of protocol design: layering, fragmentation and re-assembly,
  extensibility, etc.
* architectural constructs for enforcing limits on computational
  complexity
* empirical data on programming language features/programming styles
  that affect bug introduction rates (e.g., syntactic redundancy)
* systems architectures and designs based on LangSec principles
* computer languages, file formats, and network protocols built on
  LangSec principles
* re-engineering efforts of existing languages, formats, and protocols
  to reduce computational power

Chairs
PC co-chair: Gang Tan (Pennsylvania State University)
PC co-chair: Sergey Bratus (Dartmouth College)

Contact:
All questions about submissions should be emailed to the PC chairs:
Gang Tan (g...@psu.edu) and Sergey Bratus (ser...@cs.dartmouth.edu)

--

Gang (Gary) Tan
Professor, Penn State CSE and ICDS
W358 Westgate Building
http://www.cse.psu.edu/~gxt29
Tel:814-8657364

[TYPES/announce] permanent academic positions, Imperial

[Gardner, Philippa A]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear all,

[Sorry if you receive multiple postings of this email.]

I would like to draw your attention to a current  Imperial advert for several 
academic positions
(roughly equivalent to assistant/associate professor) in the Department of 
Computing at Imperial; details can be found 
here.

**Deadline: 7th January 2020**

We seek excellent applicants from all areas of Computer Science. I would very 
much like to encourage PL, theory  and verification experts to apply.  Please 
don’t hesitate to contact me, or other academics in the Department, if you have 
any questions. In particular, there are some exciting plans for growth and 
interaction with industry that we would be happy to share with you.

Best wishes,
Philippa




Professor Philippa Gardner
Department of Computing
Imperial College
180 Queen’s Gate
London
SW7 2AZ


My working day may not be the same as yours.  Please do not feel
obliged to reply to this email outside your normal working hours.

[TYPES/announce] RA positions, Imperial

[Gardner, Philippa A]

[ The Types Forum (announcements only),
 http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Hello all,

[Sorry for multiple postings.]

I have openings for two post-doctoral research positions in my Verified 
Software research group at Imperial on `Gillian: Program Correctness and 
Incorrectness', funded by Facebook, and `Gillian: Coq-Certified Compositional 
Symbolic Analysis', funded by a national fellowship. Details of these projects 
are given below.

These positions are for three years. The start date is flexible in these 
uncertain times, up to September 2021.  It is possible to start the positions 
remotely, although we are able to meet at Imperial when necessary so it might 
make sense to be in London. In fact, accommodation rents are currently very 
good (due to covid) so it is actually quite a good time to come to London.

If you are interested, please do not hesitate to contact me.

Philippa




Professor Philippa Gardner
Department of Computing
Imperial College
180 Queen’s Gate
London
SW7 2AZ


My working day may not be the same as yours.  Please do not feel
obliged to reply to this email outside your normal working hours.



-


Gillian: Program Correctness and Incorrectness
Philippa Gardner
Imperial College London

We have introduced Gillian [1], a multi-language platform for compositional 
symbolic analysis. It supports three flavours of analysis: whole-program 
symbolic testing; full verification based on
separation logic; and automatic compositional testing based on bi-abduction. It 
is underpinned by a core symbolic execution engine, parametric on the memory 
model of the target language, with strong mathematical foundations that unifies 
symbolic testing and verification. Gillian has been instantiated to the 
real-world languages C and JavaScript, obtaining results on real-world code 
that demonstrate the viability of our unified, parametric approach.

Meanwhile, O’Hearn [2] has observed that program correctness for describing the 
absence of bugs and program incorrectness for describing the presence of bugs 
are two sides of the same coin. He, Azalea Raad (Imperial) and others [3] have 
recently introduced incorrectness separation logic for reasoning about program 
incorrectness, in contrast with Hoare logic and separation logic for reasoning 
about program correctness. The underlying theory of Gillian resonates with the 
fundamental ideas of incorrectness logic, suggesting that Gillian has an 
unexplored potential for reasoning about both program correctness and 
incorrectness.

Our goal is to establish Gillian as a leading academic platform for integrated 
analysis of program correctness and incorrectness, by advancing the development 
of its existing analyses and incorporating the new ideas arising from 
incorrectness logic. This research position is for three years. It would suit 
someone with a strong background in formal methods (theory and/or practice), 
especially someone with experience in program analysis, testing or 
verification. It is funded by Facebook.

References

[1] Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose 
Fragoso Santos, Peter Maksimovic, Sacha-Elie Ayoun and Philippa Gardner, 
PLDI'2020. Part 2 on verification and bi-abduction is being written now! We are 
giving a talk on Gillian at the conference Rebase,
associated with ECOOP and OOPSLA, on 16th and 17th November, and at the 
Facebook Testing and Verification Symposium in December, 2020.

[2] Incorrectness Logic, Peter O'Hearn, POPL'20.

[3] Local Reasoning about the Presence of Bugs: Incorrectness Separation Logic, 
Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O'Hearn and 
Jules Villard, CAV'20.



-


Gillian: Coq-Certifiction of Compositional Symbolic Analysis
Philippa Gardner
Imperial College London

We have introduced Gillian [1], a multi-language platform for compositional 
symbolic analysis. It supports three flavours of analysis: whole-program 
symbolic testing; full verification based on
separation logic; and automatic compositional testing based on bi-abduction. 
Gillian has been instantiated to the real-world languages C (using the 
Coq-verified CompCert compiler) and JavaScript (using our own compiler), 
obtaining results on real-world code that demonstrate
the viability of our unified, parametric approach.

The goal is to provide Coq-certification for the Gillian platform. Gillian is 
underpinned by a core symbolic execution engine, parametrised by the memory 
model of the target language, with strong mathematical foundations that unifies 
symbolic testing and verification. This core is ripe for Coq mechanisation 
since it has a general correctness result that depends on lemmas associated 
with particular Gillian instantiations. The challenge is to understand how to 
link this Coq mechanisation of the core engine to the Gillian