jputnam (jputnam) wrote,

  • Mood:


You will read Software and Hospitals. Now. If you care about high security and high reliability software. You will read it now.

I think I can stick within 3 type bits. Unsigned ints don't matter, I think, and I need a code type, so

000 signed int
001 float
010 code
011 pointer to code
100 pointer to atom (int or float)
101 pointer to pointer
110 pointer to structure element
111 structure limit (length or last element; I'm not sure)

This is quite limiting; I would rather just go with four tag bits.

Anyway, from my notes (for a simple register machine)

0000 0000  0xxx xxxx zero argument operations
0000 0000  1iii iiii swi
0000 0001  rrrr xxxx one argument operations
0000 001x  dddd ssss strings
0000 01xb  rrrr rrrr push/popm
0000 100x  dddd ssss load/store
0001 0xxx  dddd ssss register shifters
0001 1xxx  dddd iiii immediate shifters
0010 0xxx  dddd ssss register alu
0011 xxxx  iiii iiii conditional jump
01xx xiii  dddd iiii immediate alu
1iii oooo  dddd ssss mov d, s+(o<<i)

Adaptation isn't hard.
0000 0000  0xxx xxxx  zero argument operations
0000 0000  1iii iiii  swi (not sure about this--it's a continuation instruction)
0000 0001  rrrr xxxx  one argument operations
0000 001x  dddd ssss  strings (d = dest, s = source, x = copy up/down)
0000 010b  rrrr rrrr  drop multiple (b = bank)
0000 1000  rrrr ssss  store (load is a one argument instruction)
0001 0xxx  rrrr ssss  variable shifters
0001 1xxx  rrrr iiii  immediate shifters
0010 0xxx  rrrr ssss  variable alu
0011 xxxx  iiii iiii  conditional jump (security problem)
01xx xiii  rrrr iiii  immediate alu

But now we have other problems. Array lookup isn't accounted for. Instructions for the register machine were:

subtract borrow
add carry

one argument
jump indirect
jump and link indirectly
set trap target
set array bound (not necessary anymore)
set arithmetic bound (possibly never necessary)
absolute value
jump to value in register
jump and link to value in register

shift left
arithmetic shift left
shift right
arithmetic shift right
rotate left
rotate right
rotate and carry left
rotate and carry right

zero arguments
no op
interrupt return
push all
pop all
push flags
pop flags
trap overflow
untrap overflow
trap out of bounds array access
untrap out of bounds access

All the jump instructions are security problems. This problem may be solvable when the program is loaded, which brings up a good point.

Not all types need to be checked at run time. Theoretically, at least, by making relative jumps small enough that greater space exists between programs than the relative jump can cross (this includes data, since code can be written as data and then executed), relative jumps can be rendered harmless. Absolute jumps need to be such that a program cannot forge a code pointer. Actually, we need to guarantee that a program cannot forge any pointer, which is why the pointer to pointer type exists. When a program is loaded, it therefore needs to be possible to check for the presence of pointers and crash if any unsafe ones are present.

It is not at all clear to me how this should be handled.

In the assumed environment, there exist hostile programs which may collaborate to destroy the security properties of the system. There is no separation of address spaces save the type system. That's what makes it interesting.

Implementing some code in the proposed system might help clear my head.

  • Resisting the urge to rewrite

    I'm writing a parser for My Own Language, like everyone does at some point. I spent about two weeks on it, and got expressions working and a few…

  • What was I thinking?

    When I wrote "★ → ★ is not inhabited", I meant that the types that inhabit it were not inhabited themselves, since, for example,…

  • (no subject)

    Assume all values are tagged at runtime. Then ∀ a.a → a can be reduced to a:Dynamic -> b:Dynamic where tag a == tag b This is the…

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.