---

Da der sikkert er manger, der har afskrevet den ca.
uendeligt lange tråd om dialere etc., vil jeg lige
nævne, at der i et par postings faktisk blev snakket
om et nyt emne, nemlig bevisbærende kode:

<news:aghibr.1nc.3@mjoelner.aaks.aarhus.dk>
<news:ofdf24l6.fsf@hotpop.com>

For nyligt blev der postet et link til en side om
enmet på comp.os.linux.security:

<news:3CE4EAC2.DC751B66@bell-bird.com.au>
http://www-2.cs.cmu.edu/~petel/papers/pcc/pcc.html

--
Kasper Dupont -- der bruger for meget tid på usenet.
For sending spam use mailto:razor-report@daimi.au.dk

---

Kasper Dupont <kasperd@daimi.au.dk> writes:
> <news:3CE4EAC2.DC751B66@bell-bird.com.au>
> http://www-2.cs.cmu.edu/~petel/papers/pcc/pcc.html

Tak! Det var George Necula's navn jeg havde glemt :)

Det er faktisk et vældigt fascinerende emne, som jeg
på længere sigt tror meget mere på end Microsofts
simple elektroniske underskrifter på distribueret
binær kode. Disse viser ikke andet end hvem der
har lavet programmet...

Der går nok desværre lidt tid inden PPC bliver praktisk
anvendeligt :)
/L
--
Lasse Reichstein Nielsen - lrn@hotpop.com
'Faith without judgment merely degrades the spirit divine.'

---

Hej Lasse

>Det er faktisk et vældigt fascinerende emne, som jeg
>på længere sigt tror meget mere på end Microsofts
>simple elektroniske underskrifter på distribueret
>binær kode. Disse viser ikke andet end hvem der
>har lavet programmet...

>Der går nok desværre lidt tid inden PPC bliver praktisk
>anvendeligt :)

Potentialet for PPC er stort, men der er en hel del praktiske
problemer der skal løses inden det for alvor bliver anvendeligt:

(1) Først og fremmest er Necula og Lee's tilgangsvinkel temmelig
ufleksibel. De beviser der bliver lavet og sendt med koden beviser
"kun" at programmet (i sig selv) overholder en præ-defineret
sikkerhedspolitik, dvs. brugerens egen sikkerhedspolitik ikke
(nødvendigvis) bliver inddraget. Brugeren er derfor nødt til selv
at verificere, at hans/hendes sikkerhedspolitik er "kompatibel"
med den politik programmet overholder.

SVJH går beviserne i deres POPL97 artikel på at bevise, at et
stykke binært kode overholder noget der svarer til ML's
type-sikkerhed, hvilket er en God Ting(tm) men også et meget
lavniveau syn på sikkerhed.

(2) Det kan være vanskeligt at producere beviserne. De arbejder på (og
er vist også kommet et godt stykke tættere på) at lave compilere
der automatisk genererer beviset; men om det kan lade sig gøre
generelt er ikke oplagt.

(3) Pt. bruges en førsteordens logik (over assemblerkode?) til at
specificere de sikkerhedsegenskaber der skal bevises. Hvorvidt det
er stærkt nok til at udtrykke de sikkerhedsegenskaber man er
interesseret i, er heller ikke oplagt.

Uanset ovenstående er PCC stadig, IMO, en glimrende ide. På
<URL: http://seclab.cs.sunysb.edu/seclab1/research/projects/mcc.html>
kan man finde lidt om Model Carrying Code (MCC) der tager ideen om PCC
lidt videre og løfter den til systemniveau.

mvh.
/rrh
--
Rene' Rydhof Hansen | Moral victories don't count.
phone : +45 8942 3283 |
email : rrh@daimi.au.dk | -- Wisdom of the Illuminati
PGP : F70E6A25 / 6C1F 0E35 54BA 577B EAFC 0EAD 4E96 8084 F70E 6A25

---

Rene Rydhof Hansen wrote:
>
> (2) Det kan være vanskeligt at producere beviserne. De arbejder på (og
> er vist også kommet et godt stykke tættere på) at lave compilere
> der automatisk genererer beviset; men om det kan lade sig gøre
> generelt er ikke oplagt.

Det afhænger af sproget. For nogle sprog som f.eks. C er det
uafgørligt, om programmet laver tildelinger med forkerte
typer. Nogle andre sprog har et typesystem, der sikrer at
ethvert program, der kan compileres også overholder typerne.

--
Kasper Dupont -- der bruger for meget tid på usenet.
For sending spam use mailto:razor-report@daimi.au.dk

---

In <3D2DA499.4E55626F@daimi.au.dk> Kasper Dupont <kasperd@daimi.au.dk> writes:

>Rene Rydhof Hansen wrote:
>>
>> (2) Det kan være vanskeligt at producere beviserne. De arbejder på (og
>> er vist også kommet et godt stykke tættere på) at lave compilere
>> der automatisk genererer beviset; men om det kan lade sig gøre
>> generelt er ikke oplagt.

> Det afhænger af sproget. For nogle sprog som f.eks. C er det
> uafgørligt, om programmet laver tildelinger med forkerte
> typer.

Ikke forstået. C's typesystem er SVJV afgørligt? Det er korrekt, at
C's typesystem ikke er så stærkt som f.eks. ML's eller Haskell's,
hvorfor man via "interessante" programkonstruktioner kan lave sjove
ting der i andre sprog villle give en typefejl (men som stadig er
veltypet i C's typesystem). Det gør C mere fleksibelt men også mere
"farligt" at bruge.

Hvis man ønsker mere (type-)sikkerhed i C kan man evt. kaste sig over
programanalyse der, konservativt, approksimerer forskellige
køretidsaspekter ved et C program, der så videre kan bruges til at
garantere at visse fejl ikke opstår.

Problemet i forbindelse med PCC er, at de ikke "kun" er interesserede
i "almindelige" typeegenskaber men i automatisk at lade en compiler
beregne den WLP (weakest liberal precondition) der skal til for at
bevise at programmet har en given egenskab (specificeret i en speciel
førsteordenslogik). Som sagt: det er ikke oplagt, at det kan lade sig
gøre generelt.

> Nogle andre sprog har et typesystem, der sikrer at ethvert program,
> der kan compileres også overholder typerne.

Øøøøhhh... ja, C eksempelvis. Er det ikke hele pointen med statisk
typning? Men statisk typning i en compiler giver dig typisk ( ikke
et bevis (et inferenstræ) du kan bruge til at lave type-check på den
oversatte kode, hvilket er hvad PCC projektet forsøger at lave.

mvh.
/rrh
--
Rene' Rydhof Hansen
email : rrh@imm.dtu.dk

---

Rene Rydhof Hansen wrote:
>
> In <3D2DA499.4E55626F@daimi.au.dk> Kasper Dupont <kasperd@daimi.au.dk> writes:
>
> >Rene Rydhof Hansen wrote:
> >>
> >> (2) Det kan være vanskeligt at producere beviserne. De arbejder på (og
> >> er vist også kommet et godt stykke tættere på) at lave compilere
> >> der automatisk genererer beviset; men om det kan lade sig gøre
> >> generelt er ikke oplagt.
>
> > Det afhænger af sproget. For nogle sprog som f.eks. C er det
> > uafgørligt, om programmet laver tildelinger med forkerte
> > typer.
>
> Ikke forstået. C's typesystem er SVJV afgørligt? Det er korrekt, at
> C's typesystem ikke er så stærkt som f.eks. ML's eller Haskell's,
> hvorfor man via "interessante" programkonstruktioner kan lave sjove
> ting der i andre sprog villle give en typefejl (men som stadig er
> veltypet i C's typesystem). Det gør C mere fleksibelt men også mere
> "farligt" at bruge.

Jeg mener f.eks. at denne kode: { char c; *(int*)(&c)=42; }
indeholder en typefejl. Og det er generelt uafgørligt, om
den slags fejl forekommer. Typereglerne i C er afgørlige,
men de tillader nogle fejl, det er programmørens ansvar, at
undgå fejl.

>
> Hvis man ønsker mere (type-)sikkerhed i C kan man evt. kaste sig over
> programanalyse der, konservativt, approksimerer forskellige
> køretidsaspekter ved et C program, der så videre kan bruges til at
> garantere at visse fejl ikke opstår.

Ja, men du vil i så fald være nødt til at afvise nogle
korrekte programmer.

--
Kasper Dupont -- der bruger for meget tid på usenet.
For sending spam use mailto:razrep@daimi.au.dk
or mailto:mcxumhvenwblvtl@skrammel.yaboo.dk

---

Kasper Dupont <kasperd@daimi.au.dk> writes:

> Jeg mener f.eks. at denne kode: { char c; *(int*)(&c)=42; }
> indeholder en typefejl. Og det er generelt uafgørligt, om
> den slags fejl forekommer. Typereglerne i C er afgørlige,
> men de tillader nogle fejl, det er programmørens ansvar, at
> undgå fejl.

Det er vist et definitionsspørgsmål :)
Jeg ville normalt sige at en typefejl var en fejl der blev fundet
at typetjekkeren. Der er ingen *fejl* i din C-kode (i.e., det er lovligt C),
men den kan give anledning til en dynamisk/run-time fejl. Altså garanterer
C's typesystem ikke fravær af runtime-fejl, men det er også svært i et sprog
der tillader {for (i=(char*)malloc(sizeof(char));;i++) *i=0;}.

Eller, sagt på en anden måde: Det er ikke en *type*-fejl at gemme en
integer et vilkårligt sted i hukommelsen, heller ikke selvom det
tilfældigvis overlapper en char.

(Det er endda et kendt trick med union's.)

> Ja, men du vil i så fald være nødt til at afvise nogle
> korrekte programmer.

Det troede jeg egentlig var hele ideen med statisk typetjek. :)
"Err on the side of safety", og sådan.

/L
--
Lasse Reichstein Nielsen - lrn@hotpop.com
'Faith without judgment merely degrades the spirit divine.'

---

Lasse Reichstein Nielsen wrote:
>
> Kasper Dupont <kasperd@daimi.au.dk> writes:
>
> > Jeg mener f.eks. at denne kode: { char c; *(int*)(&c)=42; }
> > indeholder en typefejl. Og det er generelt uafgørligt, om
> > den slags fejl forekommer. Typereglerne i C er afgørlige,
> > men de tillader nogle fejl, det er programmørens ansvar, at
> > undgå fejl.
>
> Det er vist et definitionsspørgsmål :)

Ja. Under alle omstændigheder er det en egenskab, der
ville være interesant at kunne afgøre på compiletime,
så skal du i øvrigt være velkommen til at finde på et
bedre navn til fejlen. Desværre er det en egenskab,
som er uafgørlig, så der kommer aldrig en compiler,
der kan afgøre det korrekt i alle tilfælde.

>
> Eller, sagt på en anden måde: Det er ikke en *type*-fejl at gemme en
> integer et vilkårligt sted i hukommelsen, heller ikke selvom det
> tilfældigvis overlapper en char.

OK, så siger vi det. Har du et bedre navn til fejlen?

>
> (Det er endda et kendt trick med union's.)

I det tilfælde kan koden være korrekt, mit eksempel
indeholdt en åbenlys fejl.

>
> > Ja, men du vil i så fald være nødt til at afvise nogle
> > korrekte programmer.
>
> Det troede jeg egentlig var hele ideen med statisk typetjek. :)
> "Err on the side of safety", og sådan.

Ja.

--
Kasper Dupont -- der bruger for meget tid på usenet.
For sending spam use mailto:razrep@daimi.au.dk
or mailto:mcxumhvenwblvtl@skrammel.yaboo.dk

---

rrh@daimi.au.dk (Rene Rydhof Hansen) writes:

Hej René :)

> På
> <URL: http://seclab.cs.sunysb.edu/seclab1/research/projects/mcc.html>
> kan man finde lidt om Model Carrying Code (MCC) der tager ideen om
> PCC lidt videre og løfter den til systemniveau.

Det ser spændende ud, jeg vil kigge på det. Takker for linket :)

/L
--
Lasse Reichstein Nielsen - lrn@hotpop.com
'Faith without judgment merely degrades the spirit divine.'