[TYPES/announce] 9 PhD positions at Chalmers for web security and secure programing of IoT devices

[Alejandro Russo]

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

Dear all,

We are starting two big projects on security at Chalmers. Both of them 
leverage programming languages technology to solve security problems. 
Details below.


Best,
/Alejandro

** Apologies for multiple copies **

The Computer Science and Engineering Department, Chalmers University of
Technology is hiring:

4 PhD students in web application security

5 PhD students in secure programming of IoT devices

* Important dates:

  April 27- Deadline for first round of selection (we encourage all
 candidates to apply early, especially those who need visa
 for visiting Sweden)
  May 21 - Deadline for second round of selection
  June 1, 4 or 5 - Tentative dates for interviews

* Expected starting date: preferably around September 2018.

For details, including employment conditions and how to apply, see:



4 PhD students in web application security
--

The PhD students will join an ambitios framework project: WebSec:
Securing Web-driven Systems, conducted jointly with Uppsala
University. WebSec sets out to develop a principled security platform
for the web. WebSec will break away from temporary patches and
short-term mitigations and tackle the challenge of web security at
scale. WebSec will result in:

-Comprehensive framework for detection, mitigation, and prevention of
cross-site
 scripting (XSS) attacks, encompassing (i) Crawling 2.0 and advanced string
 constraint solving for XSS detection, (ii) flexible Content Security 
Policy

 (CSP) for XSS mitigation, and (iii) a server-side template framework
separating
 data from code for XSS prevention.

-JavaScript program analysis platform for monitoring and symbolically
executing
 JavaScript, the web's main programming language.

-Principled framework for system-wide security, enabling confinement,
tainting,
 and information-flow control mechanisms across web component boundaries,
 building on our work on JSFlow http://www.jsflow.net/

-Mechanisms for confinement and compartmentalization on the web, including
 extensions to the recently proposed COWL W3C standard
 (https://www.w3.org/TR/COWL/) and the multi-app web framework Hails
 (https://hackage.haskell.org/package/hails).

-Framework for privacy on the web, addressing user tracking while enabling
 privacy-preserving web analytics.

The PhD students will join a high-profile group of researchers on software
security. Software is often the root cause of vulnerabilities in modern
computing systems. By focusing on securing the software, we target
principled
security mechanisms that provide robust protection against large classes of
attacks.

We have a track record of successful projects with top international
partners in academia and industry, including a European project
WebSand on web application sandboxing: https://www.websand.eu/

Promotional video of Chalmers research on securing web applications:
https://vimeo.com/82206652

5 PhD students in secure programming of IoT devices
---

The PhD positions are within the recently granted project Octopi: Secure
Programming for the Internet of Things (IoT). Octopi is dedicated to
contribute
and further research on (i) utilizing high-level languages to program
constraint
devices, (ii) finding suitable programming models for IoT, and (iii)
developing
security mechanisms to obtain system-wide guarantees. The programming
language
of the project is Haskell (https://www.haskell.org/). Applicants work is
expected to range from establishing new theoretical foundations to building
mature prototypes. Octopi presents many research tracks dedicated to tackle
ambitious challenges:

- Programming model

  This track focuses on developing programming models which capture the
common
  coding patterns (and architecture) of IoT applications.

- Compilation and runtime

  Programs written in high-level languages often run in tandem with fat
runtime
  responsible to provide valuable services (e.g., safe memory
  management). Having such runtime in constraint IoT devices is simply not
  possible. This task explores mechanisms to predict resource consumption
  behavior of programs so that certain runtime services are not needed, 
thus

  reducing their size.

- Locality of data

  In data-driven IoT systems, users must be able to express and control
easily
  is the choice of whether to migrate data to functions or functions to
  data. This task focus on finding ways to provide such control without
giving
  up the benefits of programming in a high-level language.

- Hardware support

  This task is aimed at the end points of IoT system. It plans on 

[TYPES/announce] PostDoc Position on Formally Secure Compilation at Inria Paris

[Catalin Hritcu]

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

A Postdoctoral Researcher position is available on my secure
compilation project at Inria Paris. The project is aimed at building
the first formally secure compilation chains for realistic programming
languages like C. Such compiler chains will ensure that high-level
abstractions cannot be violated even when interacting with untrusted
low-level code or when some program components were compromised.

I am seeking exceptional candidates with a strong, internationally
competitive track record of research in programming languages, formal
verification, or security. Particularly interesting areas include:

- formal verification in a proof assistant like Coq and
  verified compilation in particular

- security foundations, e.g., reference monitoring, hyperproperties,
  noninterference, fully abstract translations

Candidates are expected to work collaboratively and help advise students.

Please see the project web page (https://secure-compilation.github.io)
for more details about the project and about such open positions.
Do not hesitate to contact me if you are interested in joining the team!

Best Regards,
Catalin Hritcu

[TYPES/announce] 11th Interaction and Concurrency Experience (ICE 2018): 2nd CfP

[bart]

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


  ICE 2018

11th Interaction and Concurrency Experience

   June 20-21, 2018, Madrid, Spain

 Satellite workshop of DisCoTec 2018

http://2018.discotec.org/cfp_w_ice.html



=== Highlights ===


- Distinctive selection procedure involving friendly forum interaction

- ICE welcomes full papers to be included in the proceedings

- ICE also welcomes oral communications of already published or 
preliminary work


- Submission deadline: April 9 (abstracts) April 13 (papers)  ***EXTENDED***

- Invited talks: Elvira Albert, Silvia Crafa, and Alexey Gotsman

- Publication in EPTCS

- Special issue in the Journal of Logical and Algebraic Methods in 
Programming (Elsevier) (to be confirmed)




=== Important Dates ===


April 9, 2018...Abstract submission

April 13, 2018...Paper submission

April 13-May 11, 2018Reviews and PC discussion

May 14, 2018...Notification to authors

June 20-21, 2018.ICE in Madrid

July 15, 2018…...Camera-ready for post-proceedings



=== Scope ===


Interaction and Concurrency Experiences (ICEs) is a series of 
international scientific meetings oriented to theoretical computer 
science researchers with special interest in models, verification, 
tools, and programming primitives for complex interactions.



The general scope of the venue includes theoretical and applied aspects 
of interactions and the synchronization mechanisms used among components 
of concurrent/distributed systems, related to several areas of computer 
science in the broad spectrum ranging from formal specification and 
analysis to studies inspired by emerging computational models.



We solicit contributions relevant to Interaction and Concurrency, 
including but not limited to:


* Formal semantics

* Process algebras and calculi

* Models and languages

* Protocols

* Logics and types

* Expressiveness

* Model transformations

* Tools, implementations, and experiments

* Specification and verification

* Coinductive techniques

* Tools and techniques for automation

* Synthesis techniques



=== Selection Procedure ===


Since its first edition in 2008, the distinguishing feature of ICE has 
been an innovative paper selection mechanism based on an interactive, 
friendly, and constructive discussion amongst authors and PC members in 
an online forum.



During the review phase, each submission is published in a dedicated 
discussion forum. The discussion forum can be accessed by the authors of 
the submission and by all PC members not in conflict with the submission 
(the forum preserves anonymity). The forum is used by reviewers to ask 
questions, clarifications, and modifications from the authors, allowing 
them better to explain and to improve all aspects of their submission. 
The evaluation of the submission will take into account not only the 
reviews, but also the outcome of the discussion.



As witnessed by the past nine editions of ICE, this procedure 
considerably improves the accuracy of the reviews, the fairness of the 
selection, the quality of camera-ready papers, and the discussion during 
the workshop.



Last year we adopted a successful light double-blind reviewing process, 
detailed below.




=== Submission Guidelines ===


We invite two types of submissions:


- Research papers, original contributions that will be published in the 
workshop post-proceedings. Research papers must not be simultaneously 
submitted to other conferences/workshops with refereed proceedings. 
Research papers should be 3-16 pages plus at most 2 pages of references. 
Short research papers are welcome; for example a 5 page short paper fits 
this category perfectly.



- Oral communicationswill be presented at the workshop, but will not 
appear in the post-proceedings. This type of contribution includes e.g. 
previously published contributions, preliminary work, and position 
papers. There is no strict page limit for this kind of submission but 
papers of 1-5 pages would be appreciated. For example, a one page 
summary of previously published work is welcome in this category.



Authors of research papers must omit their names and institutions from 
the title page, they should refer to their other work in the third 
person and omit acknowledgements that could reveal their identity or 
affiliation. The purpose is to avoid any bias based on authors’ identity 
characteristics, such as gender, seniority, or nationality, in the 
review process.  Our goal is to facilitate an unbiased approach to 
reviewing by supporting reviewers’ access to works that do not carry 
obvious references to the authors’ identities. As mentioned above, this 
is a lightweight double-blind process. Anonymization should not be a 
heavy burden for authors, and 

[TYPES/announce] CICM 2018, final CfP, Abstract submission deadline April 15, 2018

[Serge Autexier]

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

Call for Papers
 formal papers - informal papers - doctoral programme

 
 11th Conference on Intelligent Computer Mathematics
- CICM 2018 - 
   August 13-17, 2018
  RISC, Hagenberg, Austria
http://www.cicm-conference.org/2018



Digital and computational solutions are becoming the prevalent means
for the generation, communication, processing, storage and curation of
mathematical information.

CICM brings together the many separate communities that have developed
theoretical and practical solutions for mathematical applications such as
computation, deduction, knowledge management, and user interfaces.
It offers a venue for discussing problems and solutions in each of these
areas and their integration.

CICM 2018 will feature 3 invited speakers

* Akiko Aizawa, National Institute of Informatics, University of Tokyo
* Bruno Buchberger, Research Institute for Symbolic Computation, Johannes 
Kepler University
* Adri Olde Daalhuis, University of Edinburgh

and 5 affiliated workshops

* Computer Algebra in the age of Types
* Computer Mathematics in Education - Enlightenment or Incantation
* Formal Mathematics for Mathematicians
* Formal Verification of Physical Systems
* Mathematical Models and Mathematical Software as Research Data

We invite submissions in all topics relating to intelligent computer
mathematics, in particular but not limited to

* theorem proving and computer algebra
* mathematical knowledge management
* digital mathematical libraries

CICM appreciates the varying nature of the relevant research in this area and
invites submissions of very different forms:

1) Formal submissions will be reviewed rigorously and accepted papers will be
   published in a volume of Springer LNAI:

   * regular papers (up to 15 pages) present novel research results
   
   * project and survey papers (up to 15 pages + bibliography) summarize
 existing results
  
   * system and dataset descriptions (up to 5 pages) present digital artifacts

2) Informal submissions will be reviewed with a positive bias and selected for
   presentation based on their relevance for the community.
   
   * informal papers may present work-in-progress, project announcements, 
 position statements, etc.

   * posters, mini-tutorials, and system demos will be presented in special 
sessions

3) The doctoral programme provides PhD students a forum to present early results
   receive constructive feedback and mentoring.

* Important Dates *

 Formal submissions
 
  - Abstract deadline:April 15
  - Full paper deadline:  April 22
  - Reviews sent to authors:  May 21
  - Rebuttals due:May 27
  - Notification of acceptance:   June 4
  - Camera-ready copies due:  June 8
  - Conference:   August 13-17

Informal submissions and doctoral programme

  Two separate submission rounds are offered so that some authors can make early
  travel plans while others submit spontaneously.
  
  - First round submission deadline:  April 22
  - Second round submission deadline: July  31 
  
All submissions should be made via easychair at 
https://easychair.org/conferences/?conf=cicm2018

[TYPES/announce] iFM 2081 Call For Papers

[Hao Wu]

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

===
 CALL FOR PAPERS
 iFM 2018 

 14th International Conference on integrated Formal Methods 
   September 5-7, 2018, Maynooth, Ireland

https://ifm2018.cs.nuim.ie/
===

=== Important dates ===

Abstract submission: Monday, 16 April 2018
Paper submission: Friday, 20 April 2018
Notification: Thursday, 14 June 2018
Conference: 5-7 September 2018

== Keynote speakers ==

- Cristian Cadar, Imperial College London
- Ana Cavalcanti, University of York
- Viktor Vafeiadis, MPI-SWS

== Colocated events ==

- PhD Symposium
- FMICS: International Conference on Formal Methods for 
 Industrial Critical Systems

=== Objectives and scope ===

Applying formal methods may involve the usage of different formalisms
and different analysis techniques to validate a system, either because
individual components are most amenable to one formalism or technique,
because one is interested in different properties of the system, or
simply to cope with the sheer complexity of the system. The iFM
conference series seeks to further research into hybrid approaches to
formal modeling and analysis: the combination of (formal and
semi-formal) methods for system development, regarding both modeling
and analysis. The conference covers all aspects from language design
through verification and analysis techniques to tools and their
integration into software engineering practice.

Areas of interest include but are not limited to:
- Formal and semi-formal modelling notations
- Combining formal methods
- Integration of formal methods into software engineering practice
- Program verification, model checking, and static analysis
- Theorem proving, decision procedures, SAT/SMT solving 
- Runtime analysis, monitoring, and testing
- Program synthesis
- Analysis and synthesis of hybrid, embedded, probabilistic, distributed,
  or concurrent systems
- Abstraction and refinement
- Model learning and inference

=== Submission guidelines ===

iFM 2018 solicits high quality papers reporting research results
and/or experience reports related to the overall theme of formal
method integration.

We accept papers in the following categories:

 - Regular papers (limit 15 pages) on
 -  original scientific research results
 -  tools, their foundation and evaluations
 -  applications of formal methods, including rigourous evaluations

 - Short papers (limit 8 pages) on
 -  any subject of interest in the area of formal methods that can be
 described with sufficient detail within the page limit

Page limits include bibliography and any appendices. All submissions
must be original, unpublished, and not submitted for publication
elsewhere.  Each paper will undergo a thorough review process.
Submissions will be judged on the basis of significance, relevance,
correctness, originality, and clarity.

Submissions should be made using the iFM 2018 Easychair site: 

   https://easychair.org/conferences/?conf=ifm2018

Submissions must be in PDF format, using the Springer LNCS style
files.

The conference proceedings will be published in Springer's
Lecture Notes in Computer Science series.

All accepted papers must be presented at the conference. Their authors
must be prepared to sign a copyright transfer statement. At least one
author of each accepted paper must register to the conference by the
early registration date, to be indicated by the organizers, and
present the paper.

=== Organization ===

= General chair =
Rosemary Monahan, Maynooth University, Ireland

= PC chairs =
Carlo A. Furia, Chalmers University of Technology, Sweden
Kirsten Winter, University of Queensland, Australia

= Program committee =
Erika Abraham, RWTH Aachen, Germany
Bernhard Aichernig, University of Graz, Austria
Elvira Albert, Complutense University of Madrid, Spain
Domenico Bianculli, University of Luxembourg, Luxembourg
Eerke Boiten, De Montfort University, UK
Einar Broch Johnsen, University of Oslo, Norway
Maria Christakis, MPI-SWS, Germany
David Cok, GrammaTech, USA
Robert Colvin, University of Queensland, Australia
Ferruccio Damiani, University of Turin, Italy
Eva Darulova, MPI SWS, Germany
Frank de Boer, CWI Amsterdam, Netherlands
John Derrick, University of Sheffield, UK
Brijesh Dongol, Brunel University, UK
Catherine Dubois, ENSIIE, France
Diego Garbervetsky, University of Buenos Aires, Argentina
Peter Hoefner, Data61, Australia
Marieke Huisman, University of Twente, Netherlands
Rajeev Joshi, NASA JPL, USA
Nikolai Kosmatov, CEA LIST, France
Laura Kovács, Vienna University of Technology, Austria
Rustan Leino, Amazon, USA
Larissa Meinicke, University of Queensland, Australia
Dominique Mery, LORIA Nancy, France
Toby Murray, University of Melbourne, Australia
Luigia Petre, Åbo 

[TYPES/announce] FOCLASA 2018 - 2nd call for papers

[Jacopo Soldani]

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


16th International Workshop on Foundations of 
Coordination Languages and Self-adaptive systems 
(FOCLASA 2018)

Toulouse, France / June 26, 2018

http://foclasa.lcc.uma.es/ 


PUBLICATIONS 

* Publication of the proceedings in the Lecture Notes of Computer Science of 
Springer-Verlag, following the collective volumes published by STAF 
* Publication of extended versions of selected work is planned in a special 
issue of an international journal as in previous issues of FOCLASA 


IMPORTANT DATES 

* Submission of abstract: April 13, 2018 
* Submission of papers: April 20, 2018 
* Notification of acceptance: May 20, 2018 
* Final version: June 10, 2018 
* Workshop: June 26, 2018 


WORKSHOP GOALS 

Nowadays software systems are distributed, concurrent, mobile, and often 
involve the composition of heterogeneous components and stand-alone services. 
Service coordination and self-adaptation constitute the core characteristics of 
distributed and service-oriented systems. Coordination languages and formal 
approaches to modelling and reasoning about self-adaptive behaviour help to 
simplify the development of complex distributed service-based systems, enable 
functional correctness proofs and improve reusability and maintainability of 
such systems. The goal of the FOCLASA workshop is to gather researchers and 
practitioners of the aforementioned fields, to share and identify common 
problems, and to devise general solutions in the context of coordination 
languages and self-adaptive systems. 

Topics of interest include (but are not limited to): 
* Theoretical models and frameworks for component and service coordination, 
service composition, service adaptation and concurrent system modeling. 
* Applications and usability studies for the aforementioned theoretical models, 
interaction and coordination challenges in various application domains. 
* Languages and specification protocols for component and service interaction, 
their semantics, expressiveness, validation and verification, type checking, 
static and dynamic analysis. 
* "Software as a service" models (e.g., cloud computing) and dynamic software 
architectures, such as self-adaptive and self-organizing systems. 
* Tools and environments for the development of concurrent and customizable 
self-monitoring, self-adaptive and self-organizing applications. 
* Algorithms, mathematical models and realization frameworks for 
quality-of-service observation, storage, history-based analysis in 
self-adaptive systems (queuing models, load balancing, analysis of 
fault-tolerance, machine learning systems). 

Practice, experience and methodologies from the following areas are solicited 
as well: 
* Business process modelling 
* Blockchains 
* Cloud/fog/edge computing 
* Component-based systems 
* Large-scale distributed systems 
* (Micro)service-based systems 
* Multi-agent systems 
* Peer-to-peer systems 
* Self-adaptive systems 


PROCEEDINGS 

The conference proceedings will be published by Springer, in the Lecture Notes 
in Computer Science (LNCS) series. 
Extended versions of a selection of the best papers is planned to be published 
in a special issue of an international journal as in previous issues of 
FOCLASA. 


SUBMISSION INSTRUCTIONS 

Papers must be submitted electronically in PostScript or PDF by using a 
two-phase online submission process. Registration of information and and 
abstract (max. 250 words) of papers must be completed before April 13, 2018. 
Final submission of papers is due no later than April 20, 2018. All submissions 
will be handled through the EasyChair conference management system, accessible 
from the conference web site: 
http://pages.di.unipi.it/foclasa 

Contributions must be written in English and report on original, unpublished 
work not submitted for publication elsewhere. Full papers should be 15 pages 
long, including figures and references, and prepared by using Springer's LNCS 
style. Short papers (6 pages long) describing preliminary results or 
work-in-progress are encouraged as well. Submissions not adhering to the above 
specified constraints may be rejected without any review. Papers should be 
submitted as PDF or PS via EasyChair. 


PROGRAM COMMITTEE 

Co-Chairs 

Jean-Marie Jacquet, University of Namur, Belgium 
Jacopo Soldani, University of Pisa, Italy 

Members 

Gul Agha, University of Illinois at Urbana-Champaign, USA 
Pedro Alvarez, Universidad de Zaragoza, Spain 
Farhad Arbab, CWI, The Netherlands 
Simon Bliudze, INRIA Lille - Nord Europe, France 
Radu Calinescu, University of York, UK 
Javier Camara, Carnegie Mellon University, USA 
Flavio De Paoli, University of Milano, Italy 
Francisco J. Duran, Universidad de Malaga, Spain 
Erik de Vink, Eindhoven University of Technology, The Netherlands 
Schahram Dustdar, TU Wien, Austria 
Letterio Galletta, IMT Lucca, Italy 
Eva Kuhn, Vienna University of