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...

Full description

Bibliographic Details
Published in:Communications of the ACM Vol. 60; no. 8; pp. 12 - 15
Main Author: Shein, Esther
Format: Article
Published: Association for Computing Machinery Aug2017
Subjects:
Online Access:View this record in EBSCOhost
fields @attributes:
  recordID: 1
pdfLink:
plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=124418537&site=ehost-live
header:
  @attributes:
    shortDbName: hlh
    uiTerm: 124418537
    longDbName: Humanities International Complete
    uiTag: AN
  controlInfo:
    bkinfo:
    jinfo:
      jid:
        00010782
        ACM
      jtl: Communications of the ACM
      issn: 00010782
      maglogo: N
    pubinfo:
      dt: Aug2017
      vid: 60
      iid: 8
      pid: 68
      pub: Association for Computing Machinery
    artinfo:
      ui:
        124418537
        10.1145/3105423
      ppf: 12
      ppct: 3
      formats:
      tig:
        atl: Hacker-Proof Coding: Software verification helps find the faults, preventing hacks.
      aug:
        au: Shein, Esther
      su:
        Software verification
        Prevention of computer hacking
        Computer security
        Computer security vulnerabilities
        Computer security software
      sug:
        subj:
          Software verification
          Prevention of computer hacking
          Computer security
          Computer security vulnerabilities
          Computer security software
      ab: 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.
      pubtype: Periodical
      doctype: Article
      src: R
    language: English
    refInfo:
    copyright:
      @attributes:
        flag: Y
      dt:
        @attributes:
          year: 2017
    holdings:
      @attributes:
        islocal: N