[TYPES/announce] Postdoctoral Position - Error in Embedded Link

[Mislove, Michael W]

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

Dear All,
There was an error in the embedded link in the announcement I sent about the 
postdoctoral fellowship that’s open here. The corrected link is:
 https://apply.interfolio.com/41053    
Apologies for the error.
   Best regards,
   Mike Mislove

===
Michael MislovePhone: +1 504 865-5803 

Professor and Chair FAX: +1 504 865-5063 

Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm 

New Orleans, LA 70118 USA
===



smime.p7s
Description: S/MIME cryptographic signature

[TYPES/announce] Postdoctoral Position

[Mislove, Michael W]

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

Dear All,
Below is an announcement of a postdoctoral research position starting October 1 
and running through November 30, 2018. I encourage all interested parties to 
apply. 
   Thanks,
   Mike Mislove


===
Michael MislovePhone: +1 504 865-5803 

Professor and Chair FAX: +1 504 865-5063 

Department of Computer Science
Tulane University   URL: http://www.cs.tulane.edu/~mwm 

New Orleans, LA 70118 USA
===


Postdoctoral Researcher in Semantics and Tools for Quantum Programming Languages

Applications are invited for a postdoctoral position beginning October 1, 2017 
and running through November 30, 2018. The position is in the Department of 
Computer Science at Tulane University, and will be under the supervision of 
Professor Michael Mislove. 

The successful applicant will work on a project entitled "Semantics, Formal 
Reasoning, and Tool Support for Quantum Programming”. The project involves 
designing high-level semantic models and tools to support quantum functional 
programming languages. A prototype language is Proto-Quipper, which has been  
under development (http://www.mathstat.dal.ca/~selinger/quipper/ 
 ). This language uses the 
circuit model for quantum computation, and envisions languages that support 
quantum computation under classical control. The overall aim is to design 
type-safe functional programming languages for quantum computing. The project 
also involves developing the meta-theory (including categorical semantics) of 
such languages, and eventually to formalize some of the meta-theory in a proof 
assistant. The focus of the Tulane work is modeling recursion in such 
languages, which requires developing quantum domain theory, but interactions 
with other aspects of the project are expected. 

Familiarity with programming language design, and / or semantics is a 
prerequisite of the position. The latter includes categorical semantics and 
domain theory. A good knowledge of category theory is also a prerequisite. Of 
course, familiarity with quantum computing is helpful. Additional components of 
the project will address issues around quantum information such as non-locality 
and contextuality, adapting proof assistants (Coq, Agda, Lean, etc) to develop 
automated verification for quantum programming languages. 

To apply for one of this position, direct your browser to the link: 
https://apply.interfolio.com/41053 

Funding for the project comes from the DOD and the U.S. Air Force Office of 
Scientific Research. 

smime.p7s
Description: S/MIME cryptographic signature

[TYPES/announce] Postdoc opportunity at Carnegie Mellon University

[Jean Yang]

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

Hi everyone,

  We are looking for a postdoc! Please spread the word.

Best,
Jean

--
Postdoc Opportunity at Carnegie Mellon University

We are looking for a postdoctoral researcher or research engineer to work
with Professors Jean Yang , Matt Fredrikson
, and Jian Ma
 in the School of Computer Science at
Carnegie Mellon University.

The project involves applying ideas from policy-agnostic programming
 to securing health records in a realistic setting,
in collaboration with the University of Pittsburgh Medical Center. There
are two potential directions to explore: 1) system-level issues of applying
these ideas to a production system and 2) verification questions that arise
when ensuring compliance with legal policies. We are particularly
interested in applicants with strong backgrounds in either software
systems, or programming languages and verification. Experience working in
security and privacy is preferred but not required.

The initial appointment of the position is for one year, with high
likelihood of renewal for additional years. Directions of exploration for
future years include, but are not limited to, statistical privacy and
genomic privacy. There may also be entrepreneurship opportunities relevant
to these ideas.

Please send your CV, a brief description of your interests, and contact
information of three references to Jean Yang (jyang2 [at] cs [dot] cmu
[dot] edu). Feel free to email Dr. Yang with questions.

Those curious about what Pittsburgh is like may be interested in reading this
article

about
Pittsburgh's tech article and this article

about
culture in Pittsburgh.

*Link: *http://www.cs.cmu.edu/~jyang2/opportunities/cmlh_postdoc2017.html

-- 
Jean Yang
Assistant Professor, Computer Science Department
Carnegie Mellon University
jeanyang.com | @jeanqasaur 

[TYPES/announce] QEST 2017: Call for Participation

[Ezio Bartocci]

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

[Please accept our apologies if you receive multiple copies of this message.]


CALL FOR PARTICIPATION

  QEST 2017
   14th International Conference on Quantitative Evaluation of Systems

http://qest.org/qest2017/index.html 
 


  5-7 September 2017, Harnack-Haus, Berlin, Germany


We would like to invite you to participate in the 14th International Conference 
on Quantitative Evaluation of Systems (QEST 2017). QEST is the leading forum
on quantitative evaluation and verification of computer systems and networks, 
through stochastic models and measurements. This year, QEST is part of the 
QONFEST  event, co-located 
with CONCUR, Formats, EPEW, and several workshops, 
offering great opportunities for learning, discussions, and collaborations in 
the 
vibrant city of Berlin, Germany.


== INVITED SPEAKERS ==
Morten Bisgaard, Gomspace, DK

 Romualdo Pastor-Sattoras, Universitat 
Politècnica de Catalunya, SP

Hongseok Yang, University of Oxford, UK



== PROGRAM ==
The program of QEST’17 is available at:

http://qest.org/qest2017/program.html 

== VENUE and ACCOMMODATION ==
The 14th International Conference on Quantitative Evaluation of Systems will 
be held at the Harnack-Haus. More information about the conference venue 
and hotel suggestions can be found at:

 https://conference.imp.fu-berlin.de/qonfest/venue 

 https://conference.imp.fu-berlin.de/qonfest/accomodation 


== REGISTRATION ==
Registration is now available using the web-based registration form,
with online payment on a secure website.

The early registration deadline is July 31st, 2017. More information is
available at

 https://conference.imp.fu-berlin.de/qonfest/registration-Info 


== CHAIRS and ORGANIZERS == 

General Chairs:
 Katinka Wolter (katinka.wol...@fu-berlin.de 
)
 Uwe Nestmann   (uwe.nestm...@tu-berlin.de  )

Program Chairs:
 Nathalie Bertrand (nathalie.bertr...@inria.fr 
)
 Luca Bortolussi   (l...@dmi.units.it )

[TYPES/announce] Call for Participation: Trends in Mechanized Security Proofs, TMSP'17

[Carsten Schürmann]

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

CALL FOR PARTICIPATION

TMSP'17
First International Workshop on Trends in Mechanized Secruity Proofs
(collocated  with FCSD, 2017)
Oxford, UK
3 September 2017

Recent cyber attacks against the US election have shown: the more valuable a 
target the higher the likelihood that it will be attacked. Adversaries, in 
particular nation states, have nearly unlimited capacity to devise cyberattacks 
and exploit even the smallest vulnerabilities.

In this first international workshop on Trends in Mechanized Security Proofs, 
we will discuss, how formal methods, logic, type theory, and automated 
reasoning tools can contribute to solving the security challenges of tomorrow.  
In particular, we have invited expert speakers to present

- the current state of the art in mechanized security proofs,
- rich type systems for security
- case studies in mechanized security proofs
- the formal modeling and adequacy of threat models
- security proofs in the symbolic model versus semantic security proofs

This workshop is funded by the EUTypes COST project 
(eutypes.cs.ru.nl) and co-organised by the DemTech 
project (www.demtech.dk).  For workshop details 
including registration information, please visit FCSD homepage 
(//www.cs.ox.ac.uk/conferences/fscd2017/index.html)

Best regards,
-- Herman Geuvers and Carsten Schürmann


PROGRAMME

0900-0930 REGISTRATION/TEA/COFFEE/CROISSANTS/FRUIT

0930-1015 Formal verification of cryptographic algorithms and implementations
 Gilles Barthe, IMDEA, Spain

1015-1100 Security Theorems via Model Theory
 Joshua Guttman, Worcester Polytechnic Institute, USA

1100-1130 TEA/COFFEE/BISCUITS

1130-1215 A Formal Approach to Exploiting Multi-Stage Attacks based SQL 
Injection and File-System Vulnerabilities of Web Applications
   Luca Vigano, King's College London, Great Britain

1215-1300 TBA
 Vincent Cheval
 Loria, Nancy, France

1300-1400 LUNCH

1400-1445 TBA
 Cas Cremers
 Oxford University, Great Britain

1445-1530 Verified Models and Reference Implementations for the TLS 1.3 
Standard Candidate
 Bruno Blanchet, INRIA, France

1530-1600 TEA/COFFEE/CAKE

1600-1645 Linear resolution for stateful protocols
  Eike Ritter, University of Birmingham, Great Britain

1645-1730 PSPSP: Proper Security Proofs for Stateful Protocols
  Sebastian Mödersheim, Denmark's Technical University, Denmark


ABSTRACTS

---
Title:   Formal verification of cryptographic algorithms and implementations
Speaker: Gilles Barthe

Abstract: Computer-aided cryptography develops formal methods for the design, 
analysis, and verification of cryptographic algorithms and implementations. I 
will outline some of our most recent work along these lines.

---
Title:   Security Theorems via Model Theory
Speaker: Joshua Guttmann

Abstract: We usually think of theorems as established by syntactic deduction, 
and many approaches to proving security are based on that core idea.  However, 
theorems can also follow from systematic exploration of models.

In this talk, we will explain how executions of security protocols and related 
systems can be viewed as models of suitable theories.  These models have a 
natural structure determined by their homomorphisms.

CPSA, a Cryptographic Protocol Shapes Analyzer, uses this homomorphism 
structure to control an enumeration of protocol executions.  It identifiers a 
strongest security goal achieved in each scenario it analyzes.  We extend this 
approach via more general model-finding to executions that may involve access 
control policies and other security mechanisms.

Joint work with Dan Dougherty, Moses Liskov, John Ramsdell, and Paul Rowe.


---
Title: A Formal Approach to Exploiting Multi-Stage Attacks based on SQL 
Injection and File-System Vulnerabilities of Web Applications
Speaker: Luca Vigano

Abstract: We propose a formal approach that allows one to (i) reason about 
file-system vulnerabilities of web applications and (ii) combine file-system 
vulnerabilities and SQL-Injection vulnerabilities for complex, multi-stage 
attacks. We have developed an automatic tool that implements our approach and 
we show its efficiency by discussing four real-world case studies, which are 
witness to the fact that our tool can generate, and exploit, attacks that, to 
the best of our knowledge, no other tool for the security of web applications 
can find. This is joint work with Federico De Meo and Marco Rocchetto.


---
Title: Verified Models and Reference Implementations for the TLS 1.3 Standard 
Candidate
Speaker: Bruno Blanchet