Hacker-Proof Coding: Software verification helps find the faults, preventing hacks.

The article discusses coding efforts to avoid hacking by using software verification. Software verification options are discussed including a building tool known as DeepSpec which verifies specifications, the operating system CertiKOS which uses formal verification processes to make sure code behave...

Descripción completa

Detalles Bibliográficos
Publicado en:	Communications of the ACM Vol. 60; no. 8; pp. 12 - 15
Autor principal:	Shein, Esther
Formato:	Artículo
Publicado:	Association for Computing Machinery Aug2017
Materias:	Software verification Prevention of computer hacking Computer security Computer security vulnerabilities Computer security software
Acceso en línea:	Ver este registro en EBSCOhost

Descripción
Sumario:	The article discusses coding efforts to avoid hacking by using software verification. Software verification options are discussed including a building tool known as DeepSpec which verifies specifications, the operating system CertiKOS which uses formal verification processes to make sure code behaves as it is intended, without loopholes or bugs, and an optimizing C compiler called CompCert is being evaluated to test fly-by-wire software used by aeronautics company Airbus.