Artifact Content
Not logged in

Artifact 9d520f7a84a07413c9a9b88155f603c8b2ccc243:

Wiki page [Experiment: mmmv_silkexec: spec Ideas 01] by martin_vahi on 2017-06-01 23:01:27.
D 2017-06-01T23:01:27.301
L Experiment:\smmmv_silkexec:\sspec\sIdeas\s01
P 343a7f3ede29b276a18a36a102ffdb3bf573a1e5
U martin_vahi
W 2788
<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>


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



<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>As centralized systems are centrally vulnerable, silkexapps must be
<a href="">scrutinized</a>
by multiple parties, who give them their own labels. Different parties have
different silkexapp repositories, which they assemble according to their own
trust preferences and trust calculation algorithms. Each specific version of a
silkexapp is packaged to a single Silktorrent packet. The labels from the
scrutinizing parties are given to individual Silktorrent packets, not groups of
Silktorrent packets.</p>



Z c49412c13d363060e8839e62fa90c603