Artifact Content
Not logged in

Artifact da56669af3d21cbd1bbf539e49330c76c45fa58c:

Wiki page [Experiment: mmmv_silkexec: spec Ideas 01] by martin_vahi on 2017-05-30 15:46:46.
D 2017-05-30T15:46:46.870
L Experiment:\smmmv_silkexec:\sspec\sIdeas\s01
P 7ec069676d243b0aef1fc0dae995dfaf342b30c6
U martin_vahi
W 2165
<p>This page is for a semi-random collection of ideas, how to
improve/change/create the specification of the
<a href="./wiki?name=Experiment:+mmmv_silkexec">mmmv_silkexec</a>.</p>

<p><br>
</p>

<h1>General Observations</h1>

<p>Due to the fact that applications work as a combination of application
specific code and the dependencies of the application, in some cases some code
is loaded dynamically, at runtime, a <b>proper formal verification task gets
prohibitively large pretty quickly</b>. Even, if formal verification were
possible, the <b>behavior of software packages can depend on hardware</b>,
which varies between different users. If hardware is guaranteed to be the same
for all users, for example, if all users use a specific version of the
Raspberry Pi, then the fact that <b>compile-time parameters depend on the
previously installed packages can be countered by installing all packages of
the package collection in the exact order that they were compiled and tested at
test server</b>, but even then the test server at least partly relies on the
tests that have been supplied with the software package, by the software
package creator, which may be a different person than the author of the
packaged software. It is possible for the software packager to accompany the
upstream deliverables with its own, additional, tests. <b>Tests can include
partial formal verification.</b></p>

<p>All in all <b>the general model for testing is black box testing</b>, which
may include some formal verification of some sub-components.</p>

<p><b><br>
</b></p>

<p><br>
</p>

<h1>Social Aspects Related Observations</h1>

<p>In addition to mistakes done by hardworking and meticulous persons, there
are also people, who are sloppy or who do not mind intentionally placing
malware to software packages. To avoid censorship, nothing can be banned, not
even malware. Therefore, people have to use their own choice of label
providers. The <b>task of the label providers is to analyse software packages
and label them</b> according to a labeling system of their own choice, which
can be their own custom labeling system.</p>

<p><br>
</p>

<p><br>
</p>

<p><br>
</p>

Z 67be409fadb753265fe074f8bf5c8d4e