Plessey System 250 , también conocido como PP250, fue el primer ordenador operativo que implementó el direccionamiento basado en capacidades , para comprobar y equilibrar el cálculo como una máquina Church-Turing pura . Plessey construyó los sistemas para un proyecto de enrutamiento de mensajes del ejército británico .
Una máquina de Church-Turing es una computadora digital que encapsula los símbolos en un hilo de cálculo como una cadena de abstracciones protegidas al aplicar las leyes de enlace dinámico del cálculo lambda de Alonzo Church [1]. Otras computadoras basadas en capacidades, que incluyen las computadoras CHERI y CAP , son híbridas. Conservan instrucciones predeterminadas que pueden acceder a cada palabra de la memoria física o lógica (paginada) accesible. [2]
Es una característica inevitable de la arquitectura de von Neumann [ cita requerida ] que se basa en la memoria de acceso aleatorio compartida y la confianza en los derechos de acceso predeterminados compartidos. Por ejemplo, cada palabra en cada página administrada por el administrador de memoria virtual en un sistema operativo que usa una unidad de administración de memoria (MMU) debe ser confiable. [ cita requerida ] El uso de un privilegio predeterminado entre muchos programas compilados permite que la corrupción crezca sin ningún método de detección de errores. Sin embargo, el rango de direcciones virtuales dadas a la MMU o el rango de direcciones físicas producidas por la MMU se comparte sin que la corrupción detectada fluya a través del espacio de memoria compartida de una función de software a otra. [ cita requerida ] PP250 eliminó no solo la memoria virtual [1] o cualquier sistema operativo precompilado centralizado , sino también el superusuario , eliminando todos los privilegios predeterminados de la máquina.
Son los privilegios predeterminados los que permiten el acceso no detectado de malware y hackers a una computadora. En cambio, el modelo de capacidad de objeto puro de PP250 siempre requiere una clave de capacidad limitada para definir la autoridad para operar. PP250 separó los datos binarios de los datos de capacidad para proteger los derechos de acceso, simplificar la computadora y acelerar la recolección de basura . La máquina Church encapsula y limita el contexto de la máquina de Turing al aplicar las leyes del cálculo lambda . Los medios digitales tipificados están controlados por programas mediante instrucciones de máquina claramente diferentes .
Los datos binarios mutables se programan mediante un conjunto de 28 instrucciones RISC para la programación imperativa y la programación procedimental de los datos binarios utilizando registros de datos binarios confinados a un segmento de memoria de capacidad limitada. Las claves de capacidad inmutable, exclusivas de seis instrucciones Church, navegan por el contexto computacional de una máquina de Turing a través de la estructura programada por separado del modelo de capacidad de objeto .
Las claves de capacidad inmutables representan variables de cálculo lambda con nombre. Este lado de Church es una metamáquina de cálculo lambda . El otro lado es una máquina orientada a objetos de objetos binarios, funciones programadas, listas de capacidad que definen abstracciones de funciones, almacenamiento para hilos de cálculo (aplicaciones de cálculo lambda) o almacenamiento para la lista de claves de capacidad en un espacio de nombres. Las leyes del cálculo lambda se implementan mediante las instrucciones de Church con acceso microprogramado a los registros de capacidad reservados (ocultos). El software se ensambla de forma incremental como código de máquina orientado a objetos vinculado por las claves de capacidad. La estructura de las abstracciones de funciones, incluidas las de gestión de memoria, entrada y salida, programación y servicios de comunicación, se protegen como marcos privados en un hilo. Los hilos se ejecutan en línea o como cálculos paralelos activados por instrucciones de Church controladas por programa.
En teoría, el PP250 funciona como una máquina Church-Turing funcional y segura digitalmente para software confiable. Como controlador en tiempo real , el PP250 proporcionó aplicaciones de software a prueba de fallas para sistemas de comunicación militar y telefónica computarizada con décadas de confiabilidad de software y hardware. El direccionamiento de capacidad limitada detecta y se recupera de errores en el contacto sin ninguna corrupción dañina o robo de información. Además, no existen privilegios predeterminados injustos para un sistema operativo o un superusuario, lo que bloquea todo hackeo y malware. La arquitectura de hardware de multiprocesamiento y la memoria limitada por tipo y con límites dinámicos, a la que se accede exclusivamente a través del direccionamiento de capacidad limitada, reemplazan las compilaciones lineales basadas en páginas y con límites estáticos con instrucciones con límites dinámicos, verificadas y autorizadas en tiempo de ejecución.
Al comprobar todas las referencias de memoria como un desplazamiento dentro de los tipos base, límite y de acceso especificados, los errores y ataques son detectados por el registro de capacidad de tipo limitado. Los comandos de Turing imperativos deben vincularse a objetos de datos binarios según lo definido por el registro de capacidad seleccionado. Los derechos de acceso del registro de capacidad seleccionado deben aprobar los derechos de acceso a los datos (Leer datos binarios, Escribir datos binarios o Ejecutar código de máquina). Por otro lado, las instrucciones funcionales de Church están vinculadas dinámicamente a una clave de capacidad en una lista de capacidades contenida en un registro de capacidad con derechos de acceso a la capacidad (Cargar clave de capacidad, Guardar clave de capacidad o Ingresar lista de capacidades). De esta manera, el código de máquina orientado a objetos se encapsula como una abstracción de función en el espacio de ejecución privado.
Es una arquitectura orientada a registros , con 8 registros de datos accesibles por programa y 8 registros de capacidad accesibles por programa. Los registros de datos son de 24 bits; los registros de capacidad son de 48 bits y contienen la dirección base del segmento al que se refiere la capacidad, el tamaño del segmento y los derechos de acceso otorgados por la capacidad. Las capacidades en memoria son de 24 bits y contienen los derechos de acceso y un índice en la Tabla de Capacidades del Sistema para el segmento al que se refiere la capacidad; las entradas en esa tabla contienen la dirección base del segmento y la longitud del segmento al que se refiere la entrada. [3]
Las instrucciones que acceden a la memoria tienen un código de operación , un campo que especifica un operando de registro de datos, un campo que especifica un registro de datos utilizado como registro de índice que contiene un desplazamiento hacia un segmento, un campo que especifica un registro de capacidad que hace referencia al segmento que contiene la ubicación de memoria y un campo que contiene un desplazamiento base hacia el segmento. El desplazamiento hacia el segmento es la suma del desplazamiento base y el contenido del registro de índice. [3]
El software era modular y se basaba en el modelo universal de computación y el cálculo lambda . Seis instrucciones de Church ocultaban los detalles de una aplicación de función nombrada utilizando claves de capacidad para los conceptos tipificados de variables, funciones, abstracciones, aplicaciones y un espacio de nombres. En lugar de vincular las instrucciones a la memoria lineal estática como un privilegio compartido predeterminado utilizado por malware y piratas informáticos, las instrucciones se vinculaban a objetos digitales privados, tipificados y protegidos utilizando claves de capacidad en un sistema de seguridad basado en capacidades de símbolos matemáticos inmutables. El resultado logró muchas décadas de confiabilidad de software confiable. [1]
Fabricado por la empresa Plessey plc en el Reino Unido en 1970, fue desplegado con éxito por el Ministerio de Defensa para el proyecto Ptarmigan del Ejército británico [4] y sirvió en la primera Guerra del Golfo como conmutador de red de comunicación móvil táctica .
La PP250 se vendió comercialmente alrededor de 1972.