With the recent rise of cryptocurrencies' popularity, the security and management of crypto-tokens have become critical. We have witnessed many attacks on users and providers, which have resulted in significant financial losses. To remedy these issues, several wallet solutions have been proposed. However, these solutions often lack either essential security features, usability, or do not allow users to customize their spending rules. In this paper, we propose SmartOTPs, a smart-contract wallet framework that gives a flexible, usable, and secure way of managing crypto-tokens in a self-sovereign fashion. The proposed framework consists of four components (i.e., an authenticator, a client, a hardware wallet, and a smart contract), and it provides 2-factor authentication (2FA) performed in two stages of interaction with the blockchain. To the best of our knowledge, our framework is the first one that utilizes one-time passwords (OTPs) in the setting of the public blockchain. In SmartOTPs, the OTPs are aggregated by a Merkle tree and hash chains whereby for each authentication only a short OTP (e.g., 16B-long) is transferred from the authenticator to the client. Such a novel setting enables us to make a fully air-gapped authenticator by utilizing small QR codes or a few mnemonic words, while additionally offering resilience against quantum cryptanalysis. We have made a proof-of-concept based on the Ethereum platform. Our cost analysis shows that the average cost of a transfer operation is comparable to existing 2FA solutions using smart contracts with multi-signatures.

We present DECANTeR, a system to detect anomalous outbound HTTP communication, which passively extracts fingerprints for each application running on a monitored host. The goal of our system is to detect unknown malware and backdoor communication indicated by unknown fingerprints extracted from a host's network traffic. We evaluate a prototype with realistic data from an international organization and datasets composed of malicious traffic. We show that our system achieves a false positive rate of 0.9% for 441 monitored host machines, an average detection rate of 97.7%, and that it cannot be evaded by malware using simple evasion techniques such as using known browser user agent values. We compare our solution with DUMONT [24], the current state-of-the-art IDS which detects HTTP covert communication channels by focusing on benign HTTP traffic. The results show that DECANTeR outperforms DUMONT in terms of detection rate, false positive rate, and even evasion-resistance. Finally, DECANTeR detects 96.8% of information stealers in our dataset, which shows its potential to detect data exfiltration.

Purpose The purpose of this study is to explore how the opening phrase of a phishing email influences the action taken by the recipient. Design/methodology/approach Two types of phishing emails were sent to 593 employees, who were asked to provide personally identifiable information (PII). A personalised spear phishing email opening was randomly used in half of the emails. Findings Nineteen per cent of the employees provided their PII in a general phishing email, compared to 29 per cent in the spear phishing condition. Employees having a high power distance cultural background were more likely to provide their PII, compared to those with a low one. There was no effect of age on providing the PII requested when the recipient’s years of service within the organisation is taken into account. Practical implications This research shows that success is higher when the opening sentence of a phishing email is personalised. The resulting model explains victimisation by phishing emails well, and it would allow practitioners to focus awareness campaigns to maximise their effect. Originality/value The innovative aspect relates to explaining spear phishing using four socio-demographic variables.

Aggregation of time-series data offers the possibility to learn certain statistics over data periodically uploaded by different sources. In case of privacy sensitive data, it is desired to hide every data provider's individual values from the other participants (including the data aggregator). Existing privacy preserving time-series data aggregation schemes focus on the sum as aggregation means, since it is the most essential statistics used in many applications such as smart metering, participatory sensing, or appointment scheduling. However, all existing schemes have an important drawback: they do not provide verifiable outputs, thus users have to trust the data aggregator that it does not output fake values. We propose a publicly verifiable data aggregation scheme for privacy preserving time-series data summation. We prove its security and verifiability under the XDH assumption and a widely used, strong variant of the Co-CDH assumption. Moreover, our scheme offers low computation complexity on the users' side, which is essential in many applications.

Off-the-shelf intrusion detection systems prove an ill fit for protecting industrial control systems, as they do not take their process semantics into account. Specifically, current systems fail to detect recent process control attacks that manifest as unauthorized changes to the configuration of a plant's programmable logic controllers (PLCs). In this work we present a detector that continuously tracks updates to corresponding process variables to then derive variable-specific prediction models as the basis for assessing future activity. Taking a specification-agnostic approach, we passively monitor plant activity by extracting variable updates from the devices' network communication. We evaluate the capabilities of our detection approach with traffic recorded at two operational water treatment plants serving a total of about one million people in two urban areas. We show that the proposed approach can detect direct attacks on process control, and we further explore its potential to identify more sophisticated indirect attacks on field device measurements as well.

Forensic image recognition tools are used by law enforcement agencies all over the world to automatically detect illegal images on confiscated equipment. This detection is commonly done with the help of a strictly confidential database consisting of hash values of known illegal images. To detect and mitigate the distribution of illegal images, for instance in network traffic of companies or Internet service providers, it is desirable to outsource the recognition of illegal images to these companies. However, law enforcement agencies want to keep their hash databases secret at all costs as an unwanted release may result in misuse which could ultimately render these databases useless. We present SOFIR, a tool for the Secure Outsourcing of Forensic Image Recognition allowing companies and law enforcement agencies to jointly detect illegal network traffic at its source, thus facilitating immediate regulatory actions. SOFIR cryptographically hides the hash database from the involved companies. At fixed intervals, SOFIR sends out an encrypted report to the law enforcement agency that only contains the number of found illegal images in the given interval, while otherwise keeping the company's legal network traffic private. Our experimental results show the effectiveness and practicality of our approach in the real-world.

Searchable Symmetric Encryption (SSE) allows a client to store encrypted data on a storage provider in such a way, that the client is able to search and retrieve the data selectively without the storage provider learning the contents of the data or the words being searched for. Practical SSE schemes usually leak (sensitive) information during or after a query (e.g., the search pattern). Secure schemes on the other hand are not practical, namely they are neither efficient in the computational search complexity, nor scalable with large data sets. To achieve efficiency and security at the same time, we introduce the concept of distributed SSE (DSSE), which uses a query proxy in addition to the storage provider. We give a construction that combines an inverted index approach (for efficiency) with scrambling functions used in private information retrieval (PIR) (for security). The proposed scheme, which is entirely based on XOR operations and pseudo-random functions, is efficient and does not leak the search pattern. For instance, a secure search in an index over one million documents and 500 keywords is executed in less than 1 second.

SUMMARY Adt is a simple tool in the spirit of Lex and Yacc that makes monomorphic algebraic data types, polymorphic built‐in types like the list and an efficient form of pattern matching available in C programs. C programs built with ADTs typically use NULL pointers only to indicate don't care values, and not as sentinels. This reduces the scope for errors involving NULL pointers. The Adt tool generates runtime checks, which catch many of the remaining NULL pointer dereferences. The runtime checks may consume a significant amount of CPU time; hence they can be switched off once the program is suitably debugged. Copyright © 2011 John Wiley & Sons, Ltd.

Practical courses in information security provide students with first-hand knowledge of technical security mechanisms and their weaknesses. However, teaching students only the technical side of information security leads to a generation of students that emphasize digital solutions, but ignore the physical and the social aspects of security. In the last two years we devised a course where students were given a practical assignment which includes a combination of physical security, social engineering and digital penetration testing. As part of the course, the students stole laptops using social engineering from unaware employees throughout the university campus. The assignment provided the students with a practical overview of security and increased their awareness of the strengths and weaknesses of security mechanisms. In this paper we present the design of the practical assignment and the observations from the execution.

ABSTRACT Key management is the pillar of a security architecture. Body sensor networks (BSNs) pose several challenges–some inherited from wireless sensor networks (WSNs), some unique to themselves–that require a new key management scheme to be tailor‐made. The challenge is taken on, and the result is KALwEN, a new parameterized key management scheme that combines the best‐suited cryptographic techniques in a seamless framework. KALwEN is user‐friendly in the sense that it requires no expert knowledge of a user, and instead only requires a user to follow a simple set of instructions when bootstrapping or extending a network. One of KALwEN's key features is that it allows sensor devices from different manufacturers, which expectedly do not have any pre‐shared secret, to establish secure communications with each other. KALwEN is decentralized, such that it does not rely on the availability of a local processing unit (LPU). KALwEN supports secure global broadcast, local broadcast, and local (neighbor‐to‐neighbor) unicast, while preserving past key secrecy and future key secrecy (FKS). The fact that the cryptographic protocols of KALwEN have been formally verified also makes a convincing case. With both formal verification and experimental evaluation, our results should appeal to theorists and practitioners alike. Copyright © 2010 John Wiley & Sons, Ltd.

For today’s organisations, having a reliable information system is crucial to safeguard enterprise revenues (think of on-line banking, reservations for e-tickets etc.). Such a system must often offer high guarantees in terms of its availability; in other words, to guarantee business continuity, IT systems can afford very little downtime. Unfortunately, making an assessment of IT availability risks is difficult: incidents affecting the availability of a marginal component of the system may propagate in unexpected ways to other more essential components that functionally depend on them. General-purpose risk assessment (RA) methods do not provide technical solutions to deal with this problem. In this paper we present the qualitative time dependency (QualTD) model and technique, which is meant to be employed together with standard RA methods for the qualitative assessment of availability risks based on the propagation of availability incidents in an IT architecture. The QualTD model is based on our previous quantitative time dependency (TD) model (Zambon et al. in BDIM ’07: Second IEEE/IFIP international workshop on business-driven IT management. IEEE Computer Society Press, pp 75–83, 2007), but provides more flexible modelling capabilities for the target of assessment. Furthermore, the previous model required quantitative data which is often too costly to acquire, whereas QualTD applies only qualitative scales, making it more applicable to industrial practice. We validate our model and technique in a real-world case by performing a risk assessment on the authentication and authorisation system of a large multinational company and by evaluating the results with respect to the goals of the stakeholders of the system. We also perform a review of the most popular standard RA methods and discuss which type of method can be combined with our technique.

Penetration tests on IT systems are sometimes coupled with physical penetration tests and social engineering. In physical penetration tests where social engineering is allowed, the penetration tester directly interacts with the employees. These interactions are usually based on deception and if not done properly can upset the employees, violate their privacy or damage their trust toward the organization and might lead to law suits and loss of productivity. We propose two methodologies for performing a physical penetration test where the goal is to gain an asset using social engineering. These methodologies aim to reduce the impact of the penetration test on the employees. The methodologies have been validated by a set of penetration tests performed over a period of two years.

Organizations rely on physical, technical and procedural mechanisms to protect their IT systems. Of all IT systems, laptops are the probably the most troublesome to protect, since they are easy to remove and conceal. When the thief has physical possession of the laptop, it is difficult to protect the data inside. Organizations open to the public, such as hospitals and universities, are easy targets for laptop thieves, since every day many people wander in the premises.

An emerging storage technology, called MEMS-based storage, promises nonvolatile storage devices with ultrahigh density, high rigidity, a small form factor, and low cost. For these reasons, MEMS-based storage devices are suitable for battery-powered mobile systems such as PDAs. For deployment in such systems, MEMS-based storage devices must consume little energy. This work mainly targets reducing the energy consumption of this class of devices. We derive the operation modes of a MEMS-based storage device and systemically devise a policy in each mode for energy saving. Three types of policies are presented: power management, shutdown, and data-layout policy. Combined, these policies reduce the total energy consumed by a MEMS-based storage device. A MEMS-based storage device that enforces these policies comes close to Flash with respect to energy consumption and response time. However, enhancement on the device level is still needed; we present some suggestions to resolve this issue.

Probes (or read/write heads) in MEMS-based storage devices are susceptible to wear. We study probe wear, and analyze the causes of probe uneven wear. We show that under real-world traces some probes can wear one order of magnitude faster than other probes leading to premature expiry of some probes. Premature expiry has severe consequences for the reliability, timing performance, energy-efficiency, and the lifetime of MEMS-based storage devices. Therefore, wear-leveling is a must to preclude premature expiry. We discuss how probe wear in MEMS-based storage is different from medium wear in Flash, calling for a different treatment. We present three policies to level probe wear. By simulation against three real-world traces, our work shows that an inevitable trade-off exists between lifetime, timing performance, and energy efficiency. The policies differ in the size of the trade-off. One of the policies maximizes the lifetime, so that it is optimal; and the other two are less optimal, and are used based on the configuration of the device.

A typical wireless sensor node has little protection against radio jamming. The situation becomes worse if energy-efficient jamming can be achieved by exploiting knowledge of the data link layer. Encrypting the packets may help to prevent the jammer from taking actions based on the content of the packets, but the temporal arrangement of the packets induced by the nature of the protocol might unravel patterns that the jammer can take advantage of, even when the packets are encrypted. By looking at the packet interarrival times in three representative MAC protocols, S-MAC, LMAC, and B-MAC, we derive several jamming attacks that allow the jammer to jam S-MAC, LMAC, and B-MAC energy efficiently. The jamming attacks are based on realistic assumptions. The algorithms are described in detail and simulated. The effectiveness and efficiency of the attacks are examined. In addition, we validate our simulation model by comparing its results with measurements obtained from actual implementation on our sensor node prototypes. We show that it takes little effort to implement such effective jammers, making them a realistic threat. Careful analysis of other protocols belonging to the respective categories of S-MAC, LMAC, and B-MAC reveals that those protocols are, to some extent, also susceptible to our attacks. The result of this investigation provides new insights into the security considerations of MAC protocols.

Because of its small form factor, high capacity, and expected low cost, MEMS-based storage is a suitable storage technology for mobile systems. MEMS-based storage devices should also be energy efficient for deployment in mobile systems. The problem is that MEMS-based storage devices are mechanical, and thus consume a large amount of energy when idle. Therefore, a power management (PM) policy is needed that maximizes energy saving while minimizing performance degradation. In this work, we quantitatively demonstrate the optimality of the fixed-timeout PM policy for MEMS-based storage devices. Because the media sled is suspended by springs across the head array in MEMS-based storage devices, we show that these devices (1) lack mechanical startup overhead and (2) exhibit small shutdown overhead. As a result, we show that the combination of a PM policy, that fixes the timeout in the range of 1--10~ms, and a shutdown policy, that exploits the springs, results in a near-optimal energy saving yet at a negligible loss in performance.

Because of its small form factor, high capacity, and expected low cost, MEMS-based storage is a suitable storage technology for mobile systems. However, flash memory may outperform MEMS-based storage in terms of performance, and energy-efficiency. The problem is that MEMS-based storage devices have a large number (i.e., thousands) of heads, and to deliver peak performance, all heads must be deployed simultaneously to access each single sector. Since these devices are mechanical and thus some housekeeping information is needed for each head, this results in a huge capacity loss and increases the energy consumption of MEMS-based storage with respect to flash.

Synchronous data flow (SDF) graphs have a simple and elegant semantics (essentially linear algebra) which makes SDF graphs eminently suitable as a vehicle for studying scheduling optimisations. We extend related work on using SPIN to experiment with scheduling optimisations aimed at minimising buffer requirements. We show that for a benchmark of commonly used case studies the performance of our SPIN based scheduler is comparable to that of state of the art research tools. The key to success is using the semantics of SDF to prove when using (even unsound and/or incomplete) optimisations are justified. The main benefit of our approach lies in gaining deep insight in the optimisations at relatively low cost.

We propose a general clustering algorithm for dynamic sensor networks, that makes localized decisions (1-hop neighbourhood) and produces disjoint clusters. The purpose is to extract and emphasise the essential clustering mechanisms common for a set of state-of-the-art algorithms, which allows for a better understanding of these algorithms and facilitates the definition and demonstration of common properties.

We show that there is a direct relation between the maximum length of the keys extracted from biometric data and the error rates of the biometric system. The length of the bio-key depends on the amount of information that can be extracted from the source data. This information can be used a-priori to evaluate the potential of the biometric data in the context of a specific cryptographic application. We model the biometric data more naturally as a continuous distribution and we give a new definition for fuzzy extractors that works better for this type of data.

We propose a method for engineering security protocols that are aware of timing aspects. We study a simplified version of the well-known Needham Schroeder protocol and the complete Yahalom protocol, where timing information allows the study of differ

Communication and node failures degrade the ability of a service discovery protocol to ensure users receive the correct service information when the service changes. We propose that service discovery protocols employ a set of recovery techniques to recover from failures and regain consistency. We use simulations to show that the type of recovery technique a protocol uses significantly impacts the performance. We benchmark the performance of our own service discovery protocol, FRODO against the performance of first generation service discovery protocols, Jini and UPnP during increasing communication and node failures. The results show that FRODO has the best overall consistency maintenance performance

We propose an energy-efficient service discovery protocol for wireless sensor networks. Our solution exploits a cluster overlay, where the clusterhead nodes form a distributed service registry. A service lookup results in visiting only the clusterhead nodes. We aim for minimizing the communication costs during discovery of services and maintenance of a functional distributed service registry. We compare theoretically and by simulation the impact of the chosen clustering algorithm on the service discovery protocol

Cryptographic algorithms play an important role in the security architecture of wireless sensor networks (WSNs). Choosing the most storage- and energy-efficient block cipher is essential, due to the facts that these networks are meant to operate without human intervention for a long period of time with little energy supply, and that available storage is scarce on these sensor nodes. However, to our knowledge, no systematic work has been done in this area so far. We construct an evaluation framework in which we first identify the candidates of block ciphers suitable for WSNs, based on existing literature and authoritative recommendations. For evaluating and assessing these candidates, we not only consider the security properties but also the storage- and energy-efficiency of the candidates. Finally, based on the evaluation results, we select the most suitable ciphers for WSNs, namely Skipjack, MISTY1, and Rijndael, depending on the combination of available memory and required security (energy efficiency being implicit). In terms of operation mode, we recommend Output Feedback Mode for pairwise links but Cipher Block Chaining for group communications.

As Service Discovery Protocols (SDP) are becoming increasingly important for ubiquitous computing, they must behave according to predefined principles. We present the functional Principles of Service Discovery for robust, registry-based service discovery. A methodology to guarantee adherence to these principles is provided and illustrated by formal verification of the principles against FRODO, an SDP built for the home environment. We show that, to make behavioral guarantees, an SDP has to be robust against network disturbances, and cannot rely only on the network layer.

We provide a novel trace semantics for positive core XPath that exposes all intermediate nodes visited by the query engine. This enables a detailed analysis of all information relevant to the query. We give two examples of such analyses in the form of access control policies. We translate positive core XPath into linear temporal logic, showing that branching structures can be linearised effectively. We use the SPIN model checker in a proof of concept implementation to resolve the queries, and to perform access control. The performance of the implementation is competitive.

The energy efficiency requirement of wireless sensor networks (WSN) is especially high because the sensor nodes are meant to operate without human intervention for a long period of time with little energy supply. Besides, available storage is scarce due to their small physical size. Therefore choosing the most storage- and energy-efficient block cipher for WSN is important. However to our knowledge so far no systematic work has been conducted in this area. We have identified the candidates of block ciphers suitable for WSN based on existing literature and authoritative recommendations. We have benchmarked these candidates and based on this benchmark, we have selected the suitable ciphers for WSN, namely Rijndael for high security and energy efficiency requirements; but MISTY1 for good storage and energy efficiency. In terms of operation mode, we recommend output feedback mode for static networks, but counter mode for dynamic networks.

A functional programming language can be taught successfully as a first language, but if there is no follow up the students do not appreciate the functional approach. Following discussions concerning this issue at the 1995 FPLE conference (Hartel & Plasmeijer, 1995), we decided to develop such a follow up by writing a book that teaches C to students who can write simple functional programs. This paper summarises the essence of our approach, which is based on program transformation, and presents our experience teaching functional C at the Universities of Southampton and Bristol.

Peer-to-peer (P2P) networks are generally considered to be free havens for pirated content, in particular with respect to music. We describe a solution for the problem of copyright infringement in P2P networks for music sharing. In particular, we propose a P2P protocol that integrates the functions of identification, tracking, and sharing of music with those of licensing, monitoring, and payment. This highly decentralized music-aware P2P protocol will allow access to large amounts of music of guaranteed quality; it merges in a natural way the policing functions for copyright protection and an efficient music-management infrastructure for the benefit of the user.

This paper describes a new mechanism to guarantee quality of service for multimedia streams in low-cost home networks. Quality of service is based on a token, of which the route in the network is determined by a distributed scheduler. The network node that has the token-the active node-can send its data during a predetermined period. The length of this period and which the node gets the token next is calculated by the scheduler in the active node. Every node has a scheduler on-board and schedules streams according to stream information from other nodes-contained in the token-and its own streams. Although other types of scheduler could be used, the token scheduler deploys a preemptive earliest deadline first strategy. This guarantees a theoretical maximum bandwidth utilization of 100 percent. The network is simulated and a prototype is built, based on low-cost ethernet hardware. Results show a high throughput with a small overhead of less than one percent per stream.

Automated Personalised Audio is a relatively new concept, currently making its debut on the Web. Personalised audio relies on the existence of information about the music (music metadata) and information about the users (listener profiles). By gathering profile information, personalised audio systems attempt to select appropriate content for each user. This paper introduces the Personal DJ architecture for personalised audio. An evaluation of the concept is presented on the basis of data gathered from user tests. These tests were performed with a prototype developed from this architecture using simple mood based music metadata.

Students often have difficulty with the minutiae of program construction. We introduce the idea of ‘Programming by Numbers’, which breaks some of the programming process down into smaller steps, giving such students a way into the process of Programming in the Small. Programming by Numbers doesnot add intellectual difficulty to learning programming, as it does not require the student to learn additional tools or theory. In fact it can be done with pencil and paper or the normal editor, and only requires the student to remember (and understand) seven simple steps. Programming by Numbers works best with languages that offer pattern matching, such as ML, or data-directed dispatching, such as Java.

The problem of partitioning grid-based applications for parallel computing can be solved easily and intuitively in a logic programming language such as Prolog, using only the single assignment property of the logic variable, and not the backtracking. We show that such a logic program can be transformed in a systematic way into a circular functional program, which runs 10 times faster than the original logic program. The transformation proceeds in a number of steps. The first step is novel, and we give a correctness proof. Our reasoning also uses a novel combination of concepts from both the logical and functional paradigms. Copyright © 1999 John Wiley & Sons, Ltd.

A lightweight tool is proposed to aid in the development of operational semantics. To use LETOS an operational semantics must be expressed in its meta-language, which itself is a superset of Miranda. The LETOS compiler is smaller than comparable tools, yet LETOS is powerful enough to support publication quality rendering using LaTeX, fast enough to provide competitive execution using Haskell, and versatile enough to support browsing of execution traces using Netscape. LETOS can be characterised as an experiment in ‘creative laziness’, showing how far one can get by gluing existing components together. The major specifications built using LETOS to-date are a smart card version of the Java Virtual Machine, a deterministic version of the π-calculus, and an electronic payment protocol. In addition, we have specified the semantics of many small programming languages and systems, totaling over 9000 lines of formal text. LETOS is unique in that it helps to check that a specification is operationally conservative. Copyright © 1999 John Wiley & Sons, Ltd.

Grover's search algorithm is designed to be executed on a quantum-mechanical computer. In this article, the probabilistic wp -calculus is used to model and reason about Grover's algorithm. It is demonstrated that the calculus provides a rigorous programming notation for modeling this and other quantum algorithms and that it also provides a systematic framework of analyzing such algorithms.

Abstract Over 25 implementations of different functional languages are benchmarked using the same program, a floating-point intensive application taken from molecular biology. The principal aspects studied are compile time and execution time for the various implementations that were benchmarked. An important consideration is how the program can be modified and tuned to obtain maximal performance on each language implementation. With few exceptions, the compilers take a significant amount of time to compile this program, though most compilers were faster than the then current GNU C compiler (GCC version 2.5.8). Compilers that generate C or Lisp are often slower than those that generate native code directly: the cost of compiling the intermediate form is normally a large fraction of the total compilation time. There is no clear distinction between the runtime performance of eager and lazy implementations when appropriate annotations are used: lazy implementations have clearly come of age when it comes to implementing largely strict applications, such as the Pseudoknot program. The speed of C can be approached by some implementations, but to achieve this performance, special measures such as strictness annotations are required by non-strict implementations. The benchmark results have to be interpreted with care. Firstly, a benchmark based on a single program cannot cover a wide spectrum of ‘typical’ applications. Secondly, the compilers vary in the kind and level of optimisations offered, so the effort required to obtain an optimal version of the program is similarly varied.

Abstract The resource constrained shortest path problem is an NP-hard problem for which many ingenious algorithms have been developed. These algorithms are usually implemented in Fortran or another imperative programming language. We have implemented some of the simpler algorithms in a lazy functional language. Benefits accrue in the software engineering of the implementations. Our implementations have been applied to a standard benchmark of data files, which is available from the Operational Research Library of Imperial College, London. The performance of the lazy functional implementations, even with the comparatively simple algorithms that we have used, is competitive with a reference Fortran implementation.

Abstract Our toolkit for the design and implementation of parallel functional programs supports the stepwise development of parallel programs from a high level sequential specification to an optimised parallel implementation. The toolkit is used as follows: The algorithm to be implemented is specified in a functional language. The program is debugged and tested using an interpreter. The program is compiled for a sequential machine. Its performance is analysed and improved. Annotation‐driven transformations are applied to the program to indicate parallel tasks. Simulations at task level, basic block level and bus transaction level make it possible to analyse the parallel performance of the program at three levels of detail. When the performance is optimised using the simulators, the program is executed on a genuine parallel machine. Several programs have been developed with the toolkit. A program that simulates tidal flow in an estuary of the North sea is presented as a case study to demonstrate the merits of the toolkit when developing complex parallel programs. The toolkit not only supports the design of parallel applications, it also allows the study of important concepts in parallel computer architecture. These include the behaviour of cached memory systems, bus protocols, scheduling algorithms and memory management algorithms.

Can functional programs be used to build real applications?The mere fact that this question is being asked is encouraging.Functional programming is all too often perceived as an exotic, mostly theoretical activity that has no bearing on reality.1994 saw two events specifically devoted to answering this question.The first was the Dagstuhl workshop on 'Functional programming in the real world', and the second the creation of this special issue.During the Dagstuhl workshop some 30 applications were presented.The call for papers for this special issue attracted 21 submissions.The sheer number of people working on applications indicates that solving real problems using functional languages is now becoming a serious proposition.The contributions in this issue address several diverse application areas: nuclear physics, databases query processing, parallel vision, building a spread sheet, solid modelling and molecular biology.Several other areas such as operational research and engineering design were represented in the papers that could not be included in this issue.A number of papers were also submitted targeting typical computer science applications, such as building parsers, programming environments, and executable specifications.The six papers that make up this issue have been selected purely on the basis of the formal refereeing process.Three of the papers describe prototypes of real systems.These are the database query processing, parallel vision and molecular biology systems.The production systems, which have been developed on the basis of these prototypes are used 'in anger'.The production systems have been implemented respectively as a shell script, a parallel Occam 2 program and as a C++ program.The prototypes are either incomplete, or too slow or space hungry to be used as a real application.The other three papers describe kernel applications, that were built to gain understanding of the problem domain.These are the nuclear physics, spreadsheet and solid modelling programs.These kernel applications are not used as real applications because they are not sufficiently complete to do the job properly.

Abstract Communication lifting is a program transformation that can be applied to a synchronous process network to restructure the network. This restructuring in theory improves sequential and parallel performance. The transformation has been formally specified and proved correct and it has been implemented as an automatic program transformation tool. This tool has been applied to a small set of programs consisting of synchronous process networks. For these networks communication lifting generates parallel programs that do not require locking. Measurements indicate performance gains in practice both with sequential and parallel evaluation. Communication lifting is a worthwhile optimization to be included in a compiler for a lazy functional language.

Abstract A system based on the notion of a flow graph is used to specify formally and to implement a compiler for a lazy functional language. The compiler takes a simple functional language as input and generates C. The generated C program can then be compiled, and loaded with an extensive run‐time system to provide the facility to experiment with different analysis techniques. The compiler provides a single, unified, efficient, formal framework for all the analysis and synthesis phases, including the generation of C. Many of the standard techniques, such as strictness and boxing analyses, have been included.

Abstract The performance of program‐derived combinator graph reduction is known to be superior to that of graph reduction based on a fixed set of standard combinators. The major advantage of program‐derived combinator reduction is that it uses less transient store than standard combinator reduction. We show on what activities a combinator reduction algorithm spends its execution time. Based on this analysis we show that it depends to a large extent on the application how much faster a program will run if program‐derived combinators are used instead of standard combinators. The analysis is based on experimental evidence obtained from a small bench‐mark of medium‐size functional programs. Performance gains of up to 11 x are reported for target architectures on which each memory reference consumes one unit of time. The results are valid for implementations of combinator graph reduction that use binary graphs.

Abstract The execution has been studied of four small and four medium‐sized SASL programs, when interpreted by a variant of Turner's combinator reducer. Size, structure and composition of the combinator graph have been analysed at frequent intervals during the reduction process. The most interesting results are summarized and discussed. Nodes of the graph live rather short lives and are usually not shared. Cycles are rare, and linear lists are often short. In most aspects the behaviour of the graph is quite ordinary in the sense that a simple model is sufficient to obtain a good approximation.

A conceptual model is discussed which allows the hierarchic definition of high-level input driven objects, called input-output tools, from any set of basic input primitives. An input-output tool is defined as a named object. Its most important elements are the input rule, output rule, internal tool definitions, and a tool body consisting of executable statements. The input rule contains an expression with tool designators as operands and with operators allowing for sequencing, selection, interleaving, and repetition. Input rules are similar in appearance to production rules in grammars. The input expression specifies one or more input sequences, or input patterns, in terms of tool designators. An input parser tries, at run-time, to match (physical) input tokens against active input sequences. If a match between an input token and a tool designator is found, the corresponding tool body is executed, and the output is generated according to specifications in the tool body. The control structures in the input expression allow a variety of input patterns from any number of sources. Tool definitions may occur in-line or be stored in a library. All tools are ultimately encompassed in one tool representing the program.