Human-centric verification for software safety and security

dc.contributor.advisor Suraj C Kothari
dc.contributor.author Awadhutkar, Payas
dc.contributor.department Electrical and Computer Engineering
dc.date 2020-06-26T20:02:14.000
dc.date.accessioned 2020-06-30T03:22:27Z
dc.date.available 2020-06-30T03:22:27Z
dc.date.copyright Fri May 01 00:00:00 UTC 2020
dc.date.embargo 2020-06-23
dc.date.issued 2020-01-01
dc.description.abstract <p>Software forms a critical part of our lives today. Verifying software to avoid violations of safety and security properties is a necessary task. It is also imperative to have an assurance that the verification process was correct. We propose a human-centric approach to software verification. This involves enabling human-machine collaboration to detect vulnerabilities and to prove the correctness of the verification.</p> <p>We discuss two classes of vulnerabilities. The first class is Algorithmic Complexity Vulnerabilities (ACV). ACVs are a class of software security vulnerabilities that cause denial-of-service attacks. The description of an ACV is not known a priori. The problem is equivalent to searching for a needle in the haystack when we don't know what the needle looks like. We present a novel approach to detect ACVs in web applications. We present a case study audit from DARPA's Space/Time Analysis for Cybersecurity (STAC) program to illustrate our approach.</p> <p>The second class of vulnerabilities is Memory Leaks. Although the description of the Memory Leak (ML) problem is known, a proof of the correctness of the verification is needed to establish trust in the results. We present an approach inspired by the works of Alan Perlis to compute evidence of the verification which can be scrutinized by a human to prove the correctness of the verification. We present a novel abstraction, the Evidence Graph, that succinctly captures the verification evidence and show how to compute the evidence. We evaluate our approach against ML instances in the Linux kernel and report improvement over the state-of-the-art results. We also present two case studies to illustrate how the Evidence Graph can be used to prove the correctness of the verification.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/etd/18009/
dc.identifier.articleid 9016
dc.identifier.contextkey 18242644
dc.identifier.doi https://doi.org/10.31274/etd-20200624-188
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath etd/18009
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/32192
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/etd/18009/Awadhutkar_iastate_0097E_18796.pdf|||Fri Jan 14 21:35:32 UTC 2022
dc.subject.keywords Software Analysis
dc.subject.keywords Software Assurance
dc.subject.keywords Software Safety
dc.subject.keywords Software Security
dc.subject.keywords Software Verification
dc.title Human-centric verification for software safety and security
dc.type article
dc.type.genre thesis
dspace.entity.type Publication
relation.isOrgUnitOfPublication a75a044c-d11e-44cd-af4f-dab1d83339ff
thesis.degree.discipline Computer Engineering (Software Systems)
thesis.degree.level thesis
thesis.degree.name Doctor of Philosophy
File
Original bundle
Now showing 1 - 1 of 1
Name:
Awadhutkar_iastate_0097E_18796.pdf
Size:
1.81 MB
Format:
Adobe Portable Document Format
Description: