Plessey System 250

Plessey System 250, also known as PP250, was the first operational computer to implement capability-based addressing, to check and balance the computation as a pure Church–Turing machine. Plessey built the systems for a British Army message routing project.

Description

A Church–Turing machine is a digital computer that encapsulates the symbols in a thread of computation as a chain of protected abstractions by enforcing the dynamic binding laws of Alonzo Church's lambda calculus Other capability based computers, which includ
CHERI
and CAP computers, are hybrids. They retain default instructions that can access every word of accessible physical or logical (paged) memory.

It is an unavoidable characteristic of the von Neumann architecture that is founded on shared random access memory and trust in the sharing default access rights. For example, every word in every page managed by the virtual memory manager in an operating system using a memory management unit (MMU) must be trusted. Using a default privilege among many compiled programs allows corruption to grow without any method of error detection. However, the range of virtual addresses given to the MMU or the range of physical addresses produced by the MMU is shared undetected corruption flows across the shared memory space from one software function to another. PP250 removed not only virtual memory or any centralized, precompiled operating system, but also the superuser, removing all default machine privileges.

It is default privileges that empower undetected malware and hacking in a computer. Instead, the pure object capability model of PP250 always requires a limited capability key to define the authority to operate. PP250 separated binary data from capability data to protect access rights, simplify the computer and speed garbage collection. The Church machine encapsulates and context limits the Turing machine by enforcing the laws of the lambda calculus. The typed digital media is program controlled by distinctly different machine instructions.

Mutable binary data is programmed by 28 RISC instruction set for Imperative programming and procedural programming the binary data using binary data registers confined to a capability limited memory segment. The immutable capability keys, exclusive to six Church instructions, navigate the computational context of a Turing machine through the separately programmed structure of the object-capability model.

Immutable capability keys represent named lambda calculus variables. This Church side is a lambda calculus meta-machine. The other side is an object-oriented machine of binary objects, programmed functions, capability lists defining function abstractions, storage for threads of computation (lambda calculus applications) or storage for the list of capability keys in a namespace. The laws of the lambda calculus are implemented by the Church instructions with micro-programmed access to the reserved (hidden) capability registers. The software is incrementally assembled as object-oriented machine-code linked by the capability keys. The structure of function abstractions, including those for memory management, input, and output, scheduling and communication services are protected as private frames in a thread. Threads computer inline or as parallel computations activated by program controlled Church instruction.

Conceptually, the PP250 operates at the dead center of the Church–Turing Thesis as a digitally secure, functional Church–Turing Machine for trusted software. As a real-time controller, PP250 provided fail-safe software applications for computerized telephone and military communication systems with decades of software and hardware reliability. Capability limited addressing detects and recovers from errors on contact without any harmful corruption or information theft. Furthermore, no unfair, default privileges exist for an operating system or a superuser, thereby blocking all hacking and malware. The multiprocessing hardware architecture and the dynamically bound, type limited memory, exclusively accessed through capability limited addressing, replace the statically bound, page based linear compilations with dynamically bound instructions, crosschecked and authorized at run time.

By checking all memory references as an offset within the base, limit, and access types specified bugs, errors and attacks are detected by the type limited capability register. The imperative Turing commands must bind to binary data objects as defined by the selected capability register. The access rights of the selected capability register must approve data access rights (Read Binary Data, Write Binary Data or Execute Machine Code). On the other hand, functional Church instructions are bound dynamically to a capability key in a capability list held in a capability register with capability access rights (Load Capability Key, Save Capability Key or Enter Capability List). In this way, object-oriented machine code is encapsulated as a function abstraction in private execution space. This PP250 is unlike the stretched von Neumann architecture. Instead, a lambda calculus meta-machine scales a 'single tape' Turing machine through a DNA network of 'Enter' capability keys representing functional nodes in a lambda calculus namespace

It is a register-oriented architecture, with 8 program accessible data registers and 8 program accessible capability registers. Data registers are 24-bit; capability registers are 48-bit and contain the base address of the segment to which the capability refers, the size of the segment, and the access rights granted by the capability. Capabilities in memory are 24-bit and contain the access rights and an index into the System Capability Table for the segment to which the capability refers; entries in that table contain the segment base address and length for the segment to which the entry refers.

Instructions that access memory have an opcode, a field specifying a data register operand, a field specifying a data register used as an index register containing an offset into a segment, a field specifying a capability register referring to the segment containing the memory location, and a field containing a base offset into the segment. The offset into the segment is the sum of the base offset and the contents of the index register.

The software was modular based on the universal model of computation and the lambda calculus. Six Church instructions hide the details of a named function application using capability keys for the typed concepts of variables, functions, abstractions, applications and a namespace. Instead of binding instructions to static linear memory as a default shared privilege used by malware and hackers, instructions are bound to typed and protected, private digital objects using capability keys in a capability-based security system of immutable mathematical symbols. The result achieved many decades of trusted software reliability.

History

Manufactured by Plessey company plc in the United Kingdom in 1970, it was successfully deployed by the Ministry of Defence for the British Army Ptarmigan project and served in the first Gulf War as a tactical mobile communication network switch.

The PP250 was sold commercially circa 1972.

See also

* Army Communications and Information Systems (United Kingdom)
* Flex machine

References

External links

*

Photograph of the 250 Multiprocessor System (1975)

Book on PP250 results

{{Object-capability security

British Army equipment
Computers designed in the United Kingdom
Capability systems
History of computing in the United Kingdom
Military computers