[TYPES/announce] PhD position in Secure Software and Microarchitectures
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The Division of Theoretical Computer Science, KTH Stockholm, has a new opening for a PhD position on Secure Software and Microarchitectures. We are looking for a candidate with a strong background and interest in security, formal methods, and software analysis. The successful candidate will join a WASP project on developing theories and models for information flow properties of computer architectures, solid formal justification for existing and new countermeasures, tools to analyse secure next generation software and hardware. The project focuses on developing methods to prevent vulnerabilities like Spectre. The security and effectiveness of existing countermeasures is unknown, since they are motivated by informal arguments. In fact, new vulnerabilities that exploit new microarchitecture features or corner cases easily circumvent the countermeasures. Application deadline: 2023-09-11 Detailed description: https://urldefense.com/v3/__https://kth.varbi.com/en/what:job/jobID:651770__;!!IBzWLUs!TbudLSaBu7-qumlOhQEm-BtaFEdGBVxsPFyD311jDuf1cN1JJZsemtFzHPRbVM5IHYbD-Qf-FoCZBK7symHPFm1ST6rln4Y$
[TYPES/announce] Postdoc in System Security and Formal Methods
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, KTH is hiring one PostDoc on System Security and Formal Methods Application deadline: 19.Jun.2019, https://kth.mynetworkglobal.com/en/what:job/jobID:271049/ Starting date: By agreement (preferably September 2019) The position is supported by TrustFull, trustfull.proj.kth.se, a new project on fullstack security funded by the Swedish Foundation for Strategic Research SSF. TrustFull combines novel uses of software diversity and automated software repair with formal techniques at low level to develop new techniques for end-to-end security across the entire application stack from hardware to user level applications . Within TrustFull we implement, model, and formally verify secure system components and build models and verification tools, mainly using semiautomated theorem proving in Higher Order Logic, HOL. The research group led by professor Mads Dam and assistant professor Roberto Guanciale combines deep interest in logic, mathematics, abstract modelling and formal proofs with a strong will to apply these methods to the design, development, testing, and verification of concrete system solutions. The project involves a wide variety of challenging tasks, including theory and methods, tool development, modeling and verification of critical hardware components (cpu’s, gpu’s and devices of different types), system software development and verification, prototype implementation, and software synthesis. As part of TrustFull, there will be strong interactions with other researchers at the intersection of software engineering and software security. The postdoc will also have ample opportunity to contribute to student supervision at both PhD and MSc levels, and to assist in project development and grant applications. The position is a full-time research position for one year with a possible one-year extension. The starting date is open for discussion, though ideally we would like the successful candidate to start as soon as possible. Qualifications: Applicants must hold or be about to receive a doctoral degree in Computer Science (or equivalent). The doctoral degree must have been obtained within the last three years from the application deadline (some exceptions for special grounds, for instance sick leave and parental leave). The candidate should have a strong background from at least one of the areas of formal verification and system security. About KTH: KTH Royal Institute of Technology in Stockholm has grown to become one of Europe’s leading technical and engineering universities, as well as a key centre of intellectual talent and innovation. We are Sweden’s largest technical research and learning institution and home to students, researchers and faculty from around the world. -- Roberto Guanciale KTH.se
[TYPES/announce] PostDoc on System Security and Formal Methods
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, KTH is hiring one PostDoc on System Security and Formal Methods Application deadline: April 30, 2019, https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:261817/where:4/ Starting date: By agreement (preferably July 2019) The position is supported by TrustFull, trustfull.proj.kth.se, a new project on fullstack security funded by the Swedish Foundation for Strategic Research SSF. TrustFull combines novel uses of software diversity and automated software repair with formal techniques at low level to develop new techniques for end-to-end security across the entire application stack from hardware to user level applications . Within TrustFull we implement, model, and formally verify secure system components and build models and verification tools, mainly using semiautomated theorem proving in Higher Order Logic, HOL. The research group led by professor Mads Dam and assistant professor Roberto Guanciale combines deep interest in logic, mathematics, abstract modelling and formal proofs with a strong will to apply these methods to the design, development, testing, and verification of concrete system solutions. The project involves a wide variety of challenging tasks, including theory and methods, tool development, modeling and verification of critical hardware components (cpu’s, gpu’s and devices of different types), system software development and verification, prototype implementation, and software synthesis. As part of TrustFull, there will be strong interactions with other researchers at the intersection of software engineering and software security. The postdoc will also have ample opportunity to contribute to student supervision at both PhD and MSc levels, and to assist in project development and grant applications. The position is a full-time research position for one year with a possible one-year extension. The starting date is open for discussion, though ideally we would like the successful candidate to start as soon as possible. Qualifications: Applicants must hold or be about to receive a doctoral degree in Computer Science (or equivalent). The doctoral degree must have been obtained within the last three years from the application deadline (some exceptions for special grounds, for instance sick leave and parental leave). The candidate should have a strong background from at least one of the areas of formal verification and system security. About KTH: KTH Royal Institute of Technology in Stockholm has grown to become one of Europe’s leading technical and engineering universities, as well as a key centre of intellectual talent and innovation. We are Sweden’s largest technical research and learning institution and home to students, researchers and faculty from around the world. -- Roberto Guanciale KTH.se
[TYPES/announce] 2 PostDoc positions System Security and Formal Methods
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] Dear all, KTH is hiring 2 PostDoc positions System Security and Formal Methods Application deadline: August 02, 2018, https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:218440/type:job/where:4/apply:1 Starting date: By agreement (preferably October 2018) The position is supported by TrustFull, trustfull.proj.kth.se, a new project on fullstack security funded by the Swedish Foundation for Strategic Research SSF. TrustFull combines novel uses of software diversity and automated software repair with formal techniques at low level to develop new techniques for end-to-end security across the entire application stack from hardware to user level applications. Within TrustFull we implement, model, and formally verify secure system components and build models and verification tools, mainly using semiautomated theorem proving in Higher Order Logic, HOL. The research group led by professor Mads Dam and assistant professor Roberto Guanciale combines deep interest in logic, mathematics, abstract modelling and formal proofs with a strong will to apply these methods to the design, development, testing, and verification of concrete system solutions. The project involves a wide variety of challenging tasks, including theory and methods, tool development, modeling and verification of critical hardware components (cpu’s, gpu’s and devices of different types), system software development and verification, prototype implementation, and software synthesis. As part of TrustFull, there will be strong interactions with other researchers at the intersection of software engineering and software security. The postdoc will also have ample opportunity to contribute to student supervision at both PhD and MSc levels, to contribute to undergraduate teaching, and to assist in project development and grant applications. The position is is a full-time research position for one year with a possible one-year extension. The starting date is open for discussion, though ideally we would like the successful candidate to start as soon as possible. About KTH: KTH Royal Institute of Technology in Stockholm has grown to become one of Europe’s leading technical and engineering universities, as well as a key centre of intellectual talent and innovation. We are Sweden’s largest technical research and learning institution and home to students, researchers and faculty from around the world. -- Roberto Guanciale KTH.se
[TYPES/announce] Postdoc position in provably secure systems
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are seeking candidates for a Postdoc position in the department of computer science at KTH Royal Institute of Technology. The candidate will join the PROSPER team, led by Prof. Mads Dam and assistant professor Roberto Guanciale. Our research vision is to produce novel software and platforms that have mathematically guaranteed security properties through the use of formal modelling and verification. We are looking for highly-qualified candidates that can contribute to the work on designing and modelling of various low-level system software components, on verification on low-level code, and on the modelling and analysis of the underlying hardware platforms. KTH Royal Institute of Technology in Stockholm is the largest and oldest technical university in Sweden. No less than one-third of Sweden’s technical research and engineering education capacity at university level is provided by KTH. The application deadline is 08 Jan 2017. The starting date is open for discussion. Ideally we would like the successful candidate to start in spring 2017. The full advertisement can be found at https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:126536/ Roberto Guanciale
[TYPES/announce] PhD position in Formal Modelling and Verification for High Assurance
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] We are seeking candidates for a PhD position in the department of computer science at KTH Royal Institute of Technology. The position is fully funded and is part of a larger research project led by Professor Mads Dam. Our research vision is to produce embedded software platforms that have mathematically guaranteed security properties through the use of formal modelling and verification. We are looking for highly-qualified students that can contribute to the work on formal modelling of processor microarchitecture and on software verification. The student will be involved in (i) modelling the effects of low-level system components using interactive theorem provers, (ii) validating the formal models by checking their adherence with the real hardware, and (iii) verifying the effectiveness of new and existing countermeasures for the security threats that exploit the system components. KTH Royal Institute of Technology in Stockholm is the largest and oldest technical university in Sweden. No less than one-third of Sweden’s technical research and engineering education capacity at university level is provided by KTH. The application deadline is 30 May 2016. The starting date is open for discussion. Ideally we would like the successful candidate to start September 2016. The full advertisement can be found at https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:98977/where:4/ Roberto Guanciale
[TYPES/announce] PhD position in trustworthy embedded platforms, KTH - School of Computer Science and Communication, Stockholm, Sweden
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] The theory group at KTH, School of Computer Science and Communication, invites applications for a PhD position in trustworthy embedded platforms. The recruitment is part of the creation of the new cross-departmental Center for Resilient Critical Infrastructures, CERCES, which is concerned with the security and resilience of industrial control and information systems. The center will focus on control systems, communication networks, wireless communication, and embedded software verification. In this call, we are looking for highly-qualified students that can contribute to the work on embedded software verification. The student will join the Prosper team, a team of researchers led by Professor Mads Dam, with collaborators at the Swedish Institute of Computer Science. For examples on ongoing projects, go to prosper.sics.se and haspoc.sics.se. The present project focuses on the development of embedded software platforms, kernels, hypervisors, drivers, and applications with very high demands on security, safety, and trustworthiness, with particular focus on the critical infrastructure domain. We meet these demands through formal modelling and verification, by building models of processors, systems, and devices, by building theories and tools for low level verification, and by implementing and verifying critical software components. Application deadline: 10 July 2015 For details on the position, required qualifications, and application procedure, see https://www.kth.se/en/om/work-at-kth/lediga-jobb/what:job/jobID:67924/where:4/ Contact persons for further information: Mads Dam m...@kth.se, http://www.csc.kth.se/~mfd/ Roberto Guanciale rober...@kth.se, http://www.csc.kth.se/~robertog/
[TYPES/announce] PhD position in verification of low-level software
[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ] KTH the School of Computer Science and Communication (KTH CSC) invites applications for a PhD position in verification of low-level software. We are seeking a PhD student in computer science with specialization in software security to join the PROSPER project on provably secure execution platforms for embedded systems. The objective of the project is to build and verify low-level virtualization solutions. To realize this we work with formal verification tools (theorem provers, low level program analysis tools), we build hardware models, we develop the virtualization platforms and integrate them with existing operating systems (Linux), and we apply the provers and tools to high performance code at assembly or C level. The specific role of the PhD student we are looking forward here is to be determined, but will likely involve theory and tool development for multicore processors. The successful candidate is expected to have a strong foundational background in computer science (program logics and program verification, machine architecture, operating systems, programming) and mathematics (areas such as discrete mathematics, formal logic). Application deadline: July, 6, 2014 Start date: September 2014 Details of the application procedure can be found on our website at: http://www.kth.se/en/om/work-at-kth/vacancies/ph-d-student-in-verification-of-low-level-software-1.481486 For individual questions, the interested candidate is welcome to contact Mads Dam (m...@kth.se) or Roberto Guanciale (rober...@kth.se).
