Language Theoretic Security

Language Theoretic Security (langsec) is a methodology for ensuring security of communicating software by treating all inputs as untrusted and using formal languages to ensure the validity of transmitted messages. This project is to develop a framework (in the language of your choice) for implementing communicating systems using this methodology, guaranteeing correctness of messages either […]

Continue reading

Library support for Idris

Idris is a functional programming language developed at the University of St Andrews (and elsewhere). It has similarities with Haskell (taught as part of CS2006) but additionally has a more expressive type system which allows programmers to state properties of programs which are checkable at compile time, such as assumptions about sizes of data structures, […]

Continue reading

Static Analysis Tools for Web Programming

Static analysis involves examining a program before executing it in order to find potential errors. This includes both errors in logic, such as passing a value of the wrong type to a function, and more dangerous errors such as security vulnerabilities like potential SQL injection attacks. Web applications are particularly prone to potential security errors, […]

Continue reading

Dynamic Session Types

Types in programming languages typically describe the form of valid inputs and outputs to functions and methods. By checking types, we can check that values are being used consistently throughout a program. Typically, types are checked either statically (that is, before a program is run) or dynamically (that is, at run time, when the value […]

Continue reading