SX10: A Language for Parallel Programming with Information Security
Stefan K. Muller · 2012
Many developers of concurrent programs would like to have strong security guarantees about their programs. One such guarantee is noninterference, the notion that high-security inputs to a program can have no influence on public outputs. Noninterference is commonly guaranteed through type systems which track information flow through a program. Unfortunately, many type systems for noninterference in concurrent programs require strict conditions, such as complete observational determinism, or track the security level of information at a fine granularity, making it difficult for programmers to reason about security policies. In this thesis, we introduce SX10, a practical parallel language based on X10. X10 contains the concurrency abstraction of places, which allow computation and data to be separated across computation nodes. SX10 uses places as a security abstraction as well, with security policies specified at the granularity of places. Flows of information between places correspond to flows of information between security levels, making it easier for the type system to locate potential information leaks and determine what parts of a program must meet strong conditions. We suspect these features will also allow programmers to more easily specify security policies and write secure code. We describe a prototype implementation and two case studies which demonstrate uses of the language.