Norwegian version of this page

GoRETech: Go Runtime Enforcement Techniques (completed)

Official

The GoRETech-project is funded as a bilateral Norwegian-German cooperation within the PPP-programme for collaborative research support scheme (``Projektbezogener Personenaustausch''). The cooperation is funded by the

The planned duration of the project is 24 months, the funding period spans the years 2015 and 2016.

In a nutshell

A strong current and persisting trend in computer and software systems is the all-presence of distributed and concurrent system, as witnessed by developments for cloud computing and multi-core architectures. These developments pose serious challenges for the evolution of new programming languages and accompanying analysis methods. As a matter of fact, many languages of widespread present-day concurrency have been designed at the core for traditional von-Neumann architectures and the corresponding sequential programming paradigm, with concurrency and parallelism as mere afterthoughts.

The objective of this project is to develop and apply robust and novel analysis techniques for the highly-concurrent programming language Go, with a focus on security-related applications.

Targeting application domains like platforms for cloud computing and efficient support of recent multi-core architectures, Go is designed around clean, elegant, and well-understood concurrency primitives, in particular supporting various forms of channel communication and other concurrency abstractions, not offered by libraries, but at the \emph{core} of the language. Drawing upon experience of years of concurrency research, but without neglecting practical aspects (e.g., garbage collection, efficient execution, a clean type system, guaranteeing type safety \ldots), the open-source language quickly gained momentum, partly due to the backing of an industrial giant like Google, and partly due to the rising importance of its targeted application domains. As a result, Go has been nominated ``Language of the year'' in 2009 in the well-known TIOBE index.

Taking recent advances and contributions from both collaborating partners as starting point, the project will develop mathematically sound analysis techniques to help enforcing safety- and security-related properties in distributed Go programs. The techniques will include static techniques, based on advanced constraint-based type systems, and run-time techniques, monitoring running systems as safeguard against policy-violations.

Tags: Verification, Concurrency, Run-Time Verification, Go
Published Dec. 1, 2014 8:23 AM - Last modified Apr. 21, 2021 11:30 AM

Participants

Detailed list of participants