Lambda the Ultimate

The recent discussion around Safe and Secure Software in Ada involved some amount of discussion around what is involved in proving software secure, and what role do PLs play in this. I'd like to recommend two papers to advance this discussion:

• First, Rao & Rohatgi (2001)'s EMpowering Side-channel attacks, which discusses a fairly new technology for gathering information from running systems by monitoring their EM emissions; and
• Rae & Wildman (2003)'s A Taxonomy of Attacks on Secure Devices, which provides a synthetic classification of attacks on computer systems based on the attackers degree of access to the machinery and the attacker's objectives, and which catalogues a range of attacks into the classification.

So I hereby advance three slogans:

1. Security is physical: neither applications nor operating systems can satisfy elementary security properties, but only deployed computer systems. This is because elementary security properties are about what the attacker does, which ultimately has a physical basis;
2. Security is non-modular: Programming languages and software engineering practices can ensure that software possesses properties helpful to security, but the properties are only meaningful in the context of a strategy to ensure a computer system satisfies its security policy;
3. We should not talk of secure programming languages and secure programs, such talk does mislead; to talk instead of software being secureable might promote better understanding.

Edited following Dave Griffith's remarks.

Applied Metamodelling: A Foundation for Language Driven Development (2004)
by Tony Clark, Paul Sammut, James Willans

An excerpt:

Language-driven development is fundamentally based on the ability to rapidly design new languages and tools in a unified and interoperable manner. We argue that existing technologies do not provide this capability, but a language engineering approach based on metamodelling can. The detailed study of metamodelling and how it can realise the Language-Driven Development vision will form the focus for the remainder of this book.

In software engineering circles the term "language driven development" is synonymous with "language oriented programming", a term which LtU members are more familiar with (thanks to Martin Ward's article Language Oriented Programming which first appeared in 1994, and then Martin Fowler's essays on the topic). The book hasn't appeared on the radar here on LtU, despite 41 citations. I suspect this is due in part to only one citation at Citeseer, and the lack of cross-talk between computer scientists and software engineers.

There are a lot of similarities between the XMF language (discussion at LtU) and that of the Katahdin language (discussion at LtU). Other related discussions here at LtU, include Language Workbenches: The Killer App for DSLs - about the essay by Martin Fowler, Ralph Johnson: Language workbenches - a response to Fowler's essay, XActium - Lightweight Language Engineering? - which discusses an essay about a previous version of XMF, Generating Interpreters? , Language Oriented Programming - discusses an essay by Jetbrain's Sergey Dmitriev, "Language Oriented Programming" Meta Programming System - discussion of the Jetbrain MPS system, The DSL, MDA, UML thing again... - an older discussion on the relationship between DSLs and MDA.

(Disclaimer: Some may notice that I am mentioned on the XMF web site, but this is just because I subjected their XMF language to a number of grueling challenges which they passed with flying colors: see the language snippets in the documentation. I have no affiliation with their company.)

O'Reilly is hosting a collaborative book/wiki called Software Craftsmanship: Apprentice to Journeyman. It's structured as a series of "recipes" on how to approach different aspects of software development.

Jumbala : An Action Language for UML State Machines, Juro Dubrovin, Master's Thesis.

UML 2.0 is a language for modeling complex software systems. A UML model may describe the dynamic aspects of software as well as the static structure. We concentrate on models of reactive systems, such as embedded controllers or telecommunications switches. The behavior of such systems is modeled using UML state machines. Although UML defines the structure of state machines, it leaves open the choice of an action language,which is the language used to specify how the transitions of a state machine affect the configuration of the underlying model.

A UML action language named Jumbala is introduced. The language has been designed as part of a project where the goal is to formally analyze behavioral UML models. Jumbala is based on the Java programming language. It has nearly the same syntax and semantics for statements and expressions as Java. Some new programming constructs have been added to facilitate state machine modeling. Jumbala also supports object-oriented programming with classes and inheritance.

An interpreter that parses and executes Jumbala programs has been developed. The interpreter will be part of a prototype tool set for analyzing the behavior of reactive computer systems modeled in UML.

This is interesting because it is another example of efforts from the modeling community towards combining models and programming languages to provide a single compilable specification of software. Some of these efforts are being coordinated using the term model-driven architecture (MDA).

[edit: fixed formatting issues]

In my recent adventures researching modeling languages I came across a language not previously mentioned on Lambda-the-Ultimate.org called Kermeta. From the reference manual:

Kermeta is a Domain Specific Language dedicated to metamodel engineering. It fills the gap let by MOF which defines only the structure of meta-models, by adding a way to specify static semantic (similar to OCL) and dynamic semantic (using operational semantic in the operation of the metamodel). Kermeta uses the object-oriented paradigm like Java or Eiffel.

There is a list of published papers related to Kermeta here.

We identify the following requirements for general extension and composition of software systems:

1. Orthogonal extension: Extensions may require both new data types and new operations.
2. Type safety: Extensions cannot create run-time type errors.
3. Modularity: The base system can be extended without modifying or recompiling its code.
4. Scalability: Extensions should be scalable. The amount of code needed should be proportional to the functionality added.
5. Non-destructive extension: The base system should still be available for use within the extended system.
6. Composability of extensions.

The first three of these requirements correspond to Wadler’s expression problem. Scalability (4) is often but not necessarily satisfied by supporting separate compilation; it is important for extending large software. Non-destructive extension (5) enables existing clients of the base system and also the extended system itself to interoperate with code and data of the base system, an important requirement for backward compatibility. Nested inheritance addresses the first five requirements, but it does not support extension composition. Nested intersection adds this capability.

Dynamically discovering likely program invariants from concrete test executions has emerged as a highly promising software engineering technique. Dynamic invariant inference has the advantage of succinctly summarizing both “expected”program inputs and the subset of program behaviors that is normal under those inputs. In this paper, we introduce a technique that can drastically increase the relevance of inferred invariants, or reduce the size of the test suite required to obtain good invariants. Instead of falsifying invariants produced by pre-set patterns, we determine likely program invariants by combining the concrete execution of actual test cases with a simultaneous symbolic execution of the same tests. The symbolic execution produces abstract conditions over program variables that the concrete tests satisfy during their execution. In this way, we obtain the benefits of dynamic inference tools like Daikon: the inferred invariants correspond to the observed program behaviors. At the same time, however, our inferred invariants are much more suited to the program at hand than Daikon’s hardcoded invariant patterns. The symbolic invariants are literally derived from the program text itself, with appropriate value substitutions as dictated by symbolic execution. We implemented our technique in the DySy tool, which utilizes a powerful symbolic execution and simplification engine. The results confirm the benefits of our approach. In Daikon’s prime example benchmark, we infer the majority of the interesting Daikon invariants, while eliminating invariants that a human user is likely to consider irrelevant.

The Daikon invariant detector mentioned in the abstract is here.

Seems like a pretty straightforward idea, I guess, but as always: God is in the details.

Samurai - Protecting Critical Data in Unsafe Languages. Karthik Pattabiraman, Vinod Grover, Benjamin G. Zorn.

Programs written in type-unsafe languages such as C and C++ incur costly memory errors that result in corrupted data structures, program crashes, and incorrect results. We present a data-centric solution to memory corruption called critical memory, a memory model that allows programmers to identify and protect data that is critical for correct program execution. Critical memory defines operations to consistently read and update critical data, and ensures that other non-critical updates in the program will not corrupt it. We also present Samurai, a runtime system that implements critical memory in software. Samurai uses replication and forward error correction to provide probabilistic guarantees of critical memory semantics. Because Samurai does not modify memory operations on non-critical data, the majority of memory operations in programs run at full speed, and Samurai is compatible with third party libraries. Using both applications, including a Web server, and libraries (an STL list class and a memory allocator), we evaluate the performance overhead and fault tolerance that Samurai provides.

An acceptable overhead for the pleasure of using an unsafe language? You decide.

Rex Page, Engineering software correctness, Proceedings of the ACMS,PLAN 2005 Workshop on Functional and Declarative Programming in Education, September 25, 2005.

Software engineering courses offer one of many opportunities for
providing students with a significant experience in declarative
programming. This report discusses some results from taking
advantage of this opportunity in a two-semester sequence of
software engineering courses for students in their final year of
baccalaureate studies in computer science. The sequence is based
on functional programming using ACL2, a purely functional
subset of Common Lisp with a built-in, computational logic
developed by J Strother Moore and his colleagues over the past
three decades...

A JFP educational pearl with the same title and a similar abstract appears in Journal of Functional Programming (2007), 17: 675-68, but I haven't managed to access it yet.

I am still in the process of finding furniture etc. But at least I have an apartment now... Thanks for all the help and tips, guys!

Code Splitting for Network Bound Web 2.0 Applications. Benjamin Livshits, Chen Ding. August 2007.

Modern Web 2.0 applications such as Gmail, Live Maps, MySpace, Flickr and many others have become a common part of everyday life. These applications are network bound, meaning that their performance can and does vary a great deal based on network conditions. However, there has not been much systematic research on trying to optimize network usage of these applications to make them more responsive for end-user interactions. Interestingly enough, code itself, usually in the form of JavaScript that runs within the client browser, constitutes a significant fraction of what needs to be transferred to the client for the application to run. Therefore, one way to significantly improve the perceived client-side performance for a range ofWeb 2.0 applications is to perform judicious decomposition — or splitting — of code and only transfer the code that is necessary just before it is needed. In this paper we propose several code splitting algorithms and explore their effectiveness at improving the responsiveness of large sophisticated Web 2.0 sites.

Once upon a time there was a lot of research on mobile code. It seemed like it was going nowhere. Then came Javascript, AJAX and Web 2.0, and in a worse-is-better fashion Javascript became the mobile code platform of choice. Maybe now is a good time to resume research on the subject...