2009-12-29

translating to safe c

11.9: proj.adda/translating to safe c:

. found in log/2006.9.11:
CIL (C to C translator) http://manju.cs.berkeley.edu/cil/
--. that link is dead,
but there is an active derivative:
CCured 1.3.5 (based on CIL 1.3.5) (2007)

CCured is a source-to-source translator for C.
It analyzes the C program to determine the
smallest number of run-time checks
that must be inserted in the program
to prevent all memory safety violations.
The resulting program is memory safe,
meaning that it will stop rather than
overrun a buffer or scribble over memory that it shouldn't touch.
Many programs can be made memory-safe this way
while losing only 10...60% run-time performance
Using CCured we have found bugs that Purify misses
with an order of magnitude smaller run-time cost.
. source is at:

. a tool to ensure both temporal and spatial memory safety in C programs
through a source-to-source transformation.
. implemented in Objective Caml and uses CIL(the dead link again)
as the front end to manipulate C constructs.
. for more details of the transformation
see our ACM SIGSOFT FSE 2004 paper:
"An efficient and backwards-compatible transformation
to ensure memory safety of C programs" (pdf)

. an optimizing C-to-C compiler,
it implements the extended pointer and array access semantics needed for
efficient, reliable and immediate detection of
memory access errors in unbridled C codes.

Fail-Safe ANSI-C Compiler: An Approach to
Making C Programs Secure Progress Report (pdf)
ISBN 978-3-540-00708-1
. many approaches to safe implementations of the C language
- such as Safe C and CCured --
have been proposed and implemented. To our knowledge, however,
none of them support all the features of the ANSI C standard
and prevent all unsafe operations.
(By unsafe operations, we mean any operation that leads to
undefined behavior,
such as array boundary overrun
and dereference of a pointer in a wrong type.)
This paper describes a memory-safe implementation of the full ANSI C language.
Our implementation detects and disallows
all unsafe operations,
yet conforming to the full ANSI C standard
(including casts and unions)
and even supporting many dirty tricks
common in programs beyond ANSI C.
This is achieved using sophisticated representations
of pointers (and integers)
that contain dynamic type and size information.
We also devise several techniques
-- both compile-time and run-time --
to reduce the overhead of runtime checks.

microkernels

10.5: bk.addn/gnu`hurd:
. needs cap-based security:
who cares that it protects the kernel
if it doesn't minimize authority gen'ly
and protect your data and stability ?!

book mac security


10.17: bk.addn/mac/security:

. root is disabled on mac but with no pass;
(so anyone with access to machine can become root)
enable it just to give it a pass then disable it again .
. mac's netinfo holds your acct pass insecurely,
so don't use your acct pass
as also your keychain pass
which otherwise is much more secure .

10.19: web.addn/mac/sec:

10.21: mis.addn/mac.keychain/not secure yet:
. worrying about always allowing skype access to keychain
while also keeping it unlocked .


cap-based security employed by yahoo.com

10.24: news.addn/dev.caja/cap-based goes big-time:
to General discussions concerning capability systems ,
Discussion of E and other capability languages ,
Google Caja Discuss
date Mon, Oct 12, 2009 at 5:08 PM
subject [e-lang] Caja gadgets on Yahoo! home page!!
Caja (and thus object-capabilities) are now protecting one of the
world's top three web pages, the Yahoo! home page.

The other two top web pages are the Google search page and the
Facebook page
. The Google search page has no need for isolation.
The primary means of isolation on the
Facebook page is also Javascript-to-Javascript rewriting (their FBJS),
which is also an ocap-oriented approach in most ways. AFAICT, it is
not until you get to site #11 that you find a site needing isolation
within a page and using iframes and the same origin policy (SOP) as
the primary means of providing it. (Note that iframes/SOP is still used
as a defense-in-depth backstop for Caja on the Yahoo! home page,
just in case. And Facebook does make some use of iframes as well.)

It seems that within pages served at huge scale, ocap-oriented
JS-to-JS rewriting is now the primary means of isolation, having
overtaken and surpassed iframes and SOP. While it is way too early to
declare victory, it is not too early to applaud Yahoo! for their
tremendous progress contributing to a safer web.

addm's modular architecture

10.22: addm/modular architecture:
. another term for modular is chip-oriented;
eg, to do a tree of math op's
a link to the whole math.type subexpression
is sent to the math chip,
which is implemented as a separately compiled c module
(one that was created from code safely generated from adda.code)
. the cpu does include math types needed for address arithmetic:
int's and mod's (unsigned ints);
all mult and div is done just by shifting .
. the modularity is entirely virtual:
the cpu controls all the memory,
and modularity consists of enforcing mutually exclusive access .

addm less needed than adda

10.22: addm/purpose in relation to adda:
. adda2c (a translator from my lang' to c)
is much less work than addm (a virtual machine)
and much more needed since it is my ticket out of
the long road to mastering c or obj'c .
. when the basic functionality is in place using c,
then there'll be time for
features that require addm:
a virtual machine that lets me program at the assembly level
where I can easily support continuations,
automated programming, and an interactive translator .
. addm requires 2 projects:
the vm itself needs to be designed,
and then adda needs a backend that translates
parse.trees (etree) to addm.code .

11.10: addm/required for adde to be an IDE:
. another reason for needing vm is the ide;
. when adda is just translating to c,
then you must use c tools to debug .

parrot.platform

10.14: pos.addm/platform"parrot:
. parrot has a seemingly cool idea like .net
where you can mix libraries and lang's
because they are talking parrot's lang,
and doing so easily with high-level tools .
. however, one thing that .net has over parrot
is the idea of security through managed code:
none of the library comes from unsafe c (or needs to);
the common lang is high-level,
and all code can be auto'ly inspected for safety issues .
. adda uses the same approach
by applying cap'based security rules to code
and only then converting that code
to some platform`lang .

securing the paste.buffer

addx/soa:
10.10: addm/securing the paste.buffer:
. to support both multitasking and also be safe,
app's need their own versions of paste.buffer .
. my current idea of a security app'
would hold passes and paste them in,
and then make sure my paste.buffer was cleared,
but it can't do that if other app's
can use the paste.buffer concurrently .
[12.24:
. this is where soa comes to the rescue:
the os needs to have secured connections between each app'
with journaling and tokens that leaves a paper trail
of which app's have been communicating .
. soa has the same architecture between app's
as the internet has between websites .
]

unit testing

10.8: pos.addx/unit testing:
. another reason for unit testing is to be ultra portable:
sanity checks ensure the compiler of your new platform
is acting as expected .

open source's role in security

10.1: addx/security/open source's role:
. the thing to remember about the security of openware,
is that it doesn't mean the binary can't be obfuscated:
. the source code can tell you how the target code is dynamic,
and how the dynamism is encrypted;
so, then knowing the source doesn't provide much help
in attacking the target code .
. on the other,
suppose dynamism and encryption isn't bullet-proof?
we need to have a different view of how software works:
. what is it that is making networks unsafe?
computers could be a lot smarter;
eg, I don't have trouble authenticating
even a short vid of a family member .
10.2:
. why is it needing to be in ram?
the self-policing unit should be a rom chip,
or a flash drive that can only be accessed by
some bullet-proof authentication .

addx' filetyping

10.25: addx/filetyping:

. file`type"addx is the generic type for
files that are natively exe'able;
ie, when on a pc, .exe's are renamed .addx .
and on a mac, .app's become .addx .
. of course this naming is not imposed on the native file,
but appears with addx`file.types when viewed from within
the adde file sytem viewer .
. this naming applies only to exec'ables known to be generated by addx;
ie, when adda has generated a .c file
that was then compiled to native code,
the exec'able output of that is a .addx file .
. type"addx is a sign that the exec'able conforms to the
addx managed runtime
which is offering safety the way {mono, .net} does .
(as a sanity check it does a hash of the file to see if has been changed) .

. {adda, addm, adde} are usually in binary format
unless written to .txt files, eg, as x.adda.txt .
all addx binary formats having an exportable .txt equivalent .

. adda files open into an adde ide session
where you can modify, recompile, and rerun adda code .
. adda compiles to either c or addm,
and the c is passed to the native compiler for creating addx files
while the addm bytecode can be run by the addm vm .

. addm files open into the addm vm,
and may either start a bytecoded program,
or start up a dialog telling what the program does,
and offering the same things the context menu does:
the option to open in the ide,
where you can modify, and rerun addm code .

. adde files are saved sessions,
and therefore resume a desktop session when opened .
. windows to finder, editor, and ide are found the way you left them .

filesystem as intranet of vol's and slots

10.13: mis.adda/syntax/directory as pointer model:
. if the ptr syntax is modeled after files,
then you bump into the confusion that
although folders are impl'd as pointers,
they have {copy, cut, paste} operations
that are acting as if they were containers
just like arrays, or records .

10.17: adda/syntax/volumes as a domain class:
. to unify the files systems of the pc and unix,
removables (type"volume) should be considered to be
internet nodes of domain"vol .
. a user has, both a current vol
and a current directory within each vol .
[typical pc behavior?]

10.26: adde/fs/entity and its id:
. another dimension of file id
is the volume the file is on;
because, an owner can write to several volumes
at the same time
so is not unique .
in fact, the vol'mgt is then
both the unique and direct creator;
but, consider every file must be sync'd across multiple val's
so, like git,
the unit of creation should be considered to be
the project or db, not the file .
10.27:
. a file can be uniquely identified by
(vol name * create`time * serial#)
. the serial# is needed if the vol can create a
set of files at one time,
or if the system clock is not giving accuracy to put
every file-create in its own time slice .
content vs container:
. the create time for the file
differs from that of the contents .

10.27: adda/syntax/url` slots vs vol's:
. the url domains: {vol, slot, drive} are for local content
that is reachable by a removable disk .
. drives are plugged into slots,
and volumes (eg, disks) are plugged into drives .

11.5: adda/syntax/url/filename recursively like site name:
. suppose net syntax is recursive,
so a file can be another whole net system:
//x.com/y.com
. the first idea to flesh out is
how it could make sense to use dot notation for files
the way sites do:
subj.name.type
. when they had www.x.type,
the www (front-dotted name) meant an entity
had a library fit for world-wide webbing
. another view is that
www refers to the default app;
eg, www.google.com means google's main service (search);
but then there's other services
mail, picasa, knol, code, etc .
. sites are {processors, entities} offering various services,
so in the case of locally,
a site-style name could be used for users:
eg, dev.addn.user would be a file-system dedicated to
addn's dev'ing .

11.12: adda/syntax/url/filenames like sitenames:
. when filenames have types like websites domains,
that means they are processors,
and their domains have similar meanings:
.com is closedware,
.org is openware,
.edu is knowledgebase or expert system,
.mil is security services,
.gov is os daemons .

12.1: adda/syntax/url/the register domain:
. an url naming system should represent all address spaces as
internet nodes;
eg, registers are separate address space
and so they should have their own website in the reg domain .
. the url's protocol is really not needed;
it is indicating the communications type
and is esp'ly irrelevant when the os is the same everywhere;
but, even with a variety of os's
it seems the usual is https, and that should be the default .

12.1: adda/syntax/url/the internet root as module symbol:

. a corollary of every address space getting a web node address,
is that the internet root symbol (//)
is the prefix that identifies concurrent objects:
eg, task instances, and sharable (stateless) library units .
. additionally, (//) identifies a pointer to filesystem
such that you can have access to multiple filesytems,
each having a current working directory;
eg, //destination`= //source .
whereas, //source/ (with the (/) appended)
would indicate the root directory rather than the current working directory .
. the domain name is a type name,
so then name.domain (where the type.mark happens to be a domain name)
would declare name to be a filesystem .

. once you know that a symbol is a domain-typed obj,
when is the syntax (//name) needed ?
for recursive use of domain names,
it shows when the symbol at top level
-- the level of the internet or the system
(some of the domain names are reserved for system components) .

type a/.//?
. the // is part of address literal
so not a type name as its ambiguous

. just as (/) means ptr concept
(//) symbolizes the a modular (or removable) filesystem
a separate address space,

. every tree var is //a.tree/...
adda lib consists of nodes in the adda domain //a.adda/

automated tweaking generator

10.20: adde/space generator:
. for photo edit select a set of vars
and get a matrix of all permutations
to help speed up trial&error tweaking of var's .

key-mapped menu systems

10.19: adde/escaping with near-home keys:
. how to make it easy to get in and out of
text vs menu mode?
double enter brings up menu:
0..9 for number of enters to paste into text,
hit enter again to run the current code .
. then the rest of the menu is the familiar graphic
showing the most-used keys with icons or labels
of what function the key will launch .
. in case you weren't paying attention
and your text was accidently interpreted as commands
it has a record of your exact input
right up until the end of session
which is not something that can easily be done
without paying attention .

10.29: adde/keyboard-mapping icon sets:
. the way to select a random subset of icons quickly
is to place the icons in a matrix shaped like the keyboard map,
so each near-home key toggles the selection of an icon;
then tab.key pulls next set of icons onto the display;
finally, enter.key sets selection to paste`top .

concurrent account windows

10.17: adde/acct`windows:

. the usual acct'based security is a convenience of generics;
the app inherits the capabilities of the whatever user launched it;
this is not in itself a security curse;
rather the curse comes when
changing user acct's is not at all convenient .

. the real problem with acct'based security
is that fast user switching needs to be more than "(fast);
rather, it needs to be concurrent,
so you have can have windows into each user`acct,
rather than just one user's acct windowing multiple app's or doc's .
[10.18: -- like the windows of virtual machines .]

[10.18:
. the desktop would contain, in addition to all the volumes,
all the user folders, each representing
either a user'acct, or a user's session .
. you can create a new window by clicking on a user acct,
and if you don't already have a window into that user,
it asks you for that user's password . ]

cap'config'ed acct's:
. after the user-switching issue,
there's the problem of granularity:
. the finest granularity is capability-based addressing:
for a particular job (app call)
an app is given a particular set of tools
(readers, writers, compilers, ...)
with which to operate on particular set of obj's .
. one way to provide this cap'based addressing
-- in a convenient, generic way
that involves inheritance --
is to have, in addition to user acct's,
cap'config'ed acct's
that specify the current capabilities .
. these acct's are folders that contain config files,
such that when an app is run from that window
it inherits -- not the rights of the user --
but the allowances set forth in the config files
of the window's current cap'config acct .
[10.18:
. the quick way to set up a config file
is to simply accept an app's externals list;
eg, an editor needs access only to
( the doc's the user asked it to open
, the temp'files within its private folder, and
, some auto'backup arrangement on another volume
) .
. most app's can be defined functionally,
and the config' doesn't get too complicated . ]
. for complicated config's,
the app's externals.list could be a folder to be filled with
links to allowables .
(it could work like the directory listing command,
where listings could come with a parameter to indicate
whether it means just the files in the given folder,
or all files in all the enclosed subfolders also ) .
[10.18:
. another dimension of the cap'config'ed acct
is having the config's determine what app's are available generally,
and what app is available specifically
when a particular type of obj' is clicked . ]

smartcards

10.17: adde/smartcards:
. smartcards have at least virtual processor,
meaning that if the card can be reached by a trusted process,
... but that is a big if ! .

pasteboard and drag behaviors

10.13: adde/pasteboard and drag behaviors:
. it can be confusing to have copy|move behaviours depend on
whether the places are on the same volume or not .
. mac and pc offer various behaviors that further complicate things .
. the mac should be allowing a cut operation for folders,
and both should be following a paste with a dialog
that shows you what it's about to do,
and then does it (or your changes) when you press enter .
. of course, none of this should be hardwired;
rather you can use a gui to do things any way you choose:
{ mac, pc, customize } .
. customize will have these options:
. when I drag folders, I mean a
{cut, copy, {cut, copy} on the volume change} .

user`agent/can it be trusted?

10.1: adde/user`agent/can it be trusted?:
. one reason an app may want to do its own gui
is when it doesn't trust the environs;
eg, it may be infected by keylogger .
. with that in mind,
one must be careful about the addx architecture
appearing to have the same vulnerability as the matrix .
. some secure.wares like keepass are openware,
so there it's possible to integrate .
. it's an empty concern however,
because if addx is not controlling the whole platform;
it's discipline is applied only to
programs under it's control;
the user can still access other programs directly .
. if addx could have complete control,
there would be no way to get key.logger infections .

systemc

10.18: news.adda/systemc
. why [systemC suite]?
it helps install openware for dev'ers of systemC
the new c++ extension lang for dev'ing systems on a chip,
IEEE Std 1666TM-2005
SystemC is an ANSI standard C++ class library
for system and hardware design
for use by designers and architects who need to address
complex systems that are a hybrid between
hardware and software .
. SystemC provides a mechanism for managing this complexity
with its facility for
modeling hardware and software together
at multiple levels of abstraction.
This capability is not available in
traditional hardware description languages.

. Users are encouraged to check this for errata periodically.
downloading:
TLM_2_0_LRM.pdf TLM-2.0 Reference Manual
systemc-2.2.0.tgz Core SystemC Language and Examples, Release 2.2
TLM2_Whitepaper.pdf TLM-2 Whitepaper

web:
tlm (transaction level modeling)
-- this refers to high-level hardware simulation
vs the rtl (register transfer level) modeling done by vhdl .
. tlm is a much quicker simulator than rtl mode,
but may not give needed info about hardware timing subtleties .




systemC is replacing the specially designed HDL's
like Verilog and VHDL in many situations.
This does not mean that these HDL's are obsolete now,
instead, systemC supports a new approach to design a system.
The systemC born because of the necessities of the current electronic industry:
Previously, the C (or C++) was used to write the software part of the design.
For hardware part any of the existing HDL's were used to design the hardware.
It was very difficult to setup a testbench which is common for both,
since they are entirely different languages.
The introduction of systemC solved many of these problems.

booking unicode

9.13: Validate input# character encoding:

[12.29:
. this is an expansion of
Wheeler's how-to on secure programming
]

[9.14:
. staying in control of character encoding
can determine your effectiveness in filtering web content
for preventing cross-site scripting and semantic attacks .
]
when needing to process older documents
in various older (language-specific) character sets,
you need to ensure that an untrusted user cannot control
the setting of another document's character set .
[9.15:
. this page will explain how the various char'encodings can be tricky,
and how mistranslation can affect security .

. UCS (Universal Character Set) is the new standard (subsuming ASCII);
it's the function { integer -> image } for all the images of the world,
requiring more than 2-bytes and less than 4-bytes .

. UTF (UCS Transformation Format) is the generic name for
how to code the UCS -- there are several approaches:
the efficient and backward-compatable way is to use a variant record;
eg, UTF-8:
variant#1 is ascii in a single byte;
variant#{2..4} can be contained in {2..4} bytes, respectively .

. alt'ly, UTF-32 is simply a 4-byte integer
that maps directly to UCS values -- no decoding is needed .

. for handling international characters UTF-8 has become the standard;
. an attacker can exploit an illegal UTF-8 value
by sneaking metacharacters into the string
which can turn parameter names into arbitrary commands .

9.14: 9.15:
. for instance, the wrong way to decode the invalid UTF-8 value
0,C0,80 #16 = (110)0,0000,(10)00,0000 #2
is to remove all the discriminant bits (shown in parentheses),
and return the remaining bits (00#16);
because, the discriminant"(110) was telling you
the remaining bits should have been within 0080 ... 07FF #16;
if the result wasn't in that range, the value is illegal,
and the translator should warn the client .
9.15:
. another example relevant to security
would be filtering to prohibit the char.string that
give a unix filename reference to the parent directory "/../":
/ . . /
2F,2E, 2E,2F#16 . weak parsing could still be caught by this:
2F,C0AE,2E,2F #16 . the same string with 2E replaced by C0AE .
. then the client might misparse this invalid UTF-8 to: 2E#16
when in fact it is an illegal value .
. C0 AE = (110)0,000,(10)10,1110 -utf-8-> 10,1110#2 = 2E#16
(illegal value because for discriminant (110)
the value should be greater than 80#16, and 2E is not ) .
9.15:
. another complication is that
there are some obsolete formats to watch for:
not only does the UTF-8 conversion have to check that it's
holding the correct range of UCS values,
it also has to check for the format being UTF-16:
convert UCS-2 to UTF-8:
. UCS-2 is just the first 2 bytes of 4-byte UCS;
so the UCS conversion can be used by
extending each UCS-2 character with two zero-valued bytes: 00,00,xx,xx#16 ;
however,
pairs of UCS-2 values between D800 and DFFF need special treatment:
because, they are "(surrogate pairs)
being actually UCS-4 characters transformed through UTF-16:
. convert the UTF-16 to UTF-32,
then convert the UTF-32 to UTF-8 .
]


00 .. 1F -- C0 set
80 .. 9F -- C1 set
for compatibility with the ISO/IEC 2022 framework
-- 7F (delete) is also a sort of control char .

9.15: BOM and unicode signature U+FEFF:

. a BOM (byte order mark) is the value U+FEFF
prepended to the unicode char.string,
thereby acting as the signature of a Unicode.string
and indicating the byte ordering:
. here is the format of U+FEFF per UTF form and byte ordering:
00 00 FE FF UTF-32, big-endian
FF FE 00 00 UTF-32, little-endian
FE FF UTF-16, big-endian
FF FE UTF-16, little-endian
EF BB BF UTF-8
-- the UTF-8 format is byte-oriented,
so it is unaffected by byte ordering .
. when not at the beginning of a text stream, U+FEFF
should normally not occur.
For backwards compatibility it should be treated as
ZERO WIDTH NON-BREAKING SPACE (ZWNBSP),
and is then part of the content of the file or string.
The use of U+2060 WORD JOINER is strongly preferred over ZWNBSP
for expressing word joining semantics
since it cannot be confused with a BOM.
When designing a markup language or data protocol,
the use of U+FEFF can be restricted to that of Byte Order Mark.
In that case, any FEFF occurring in the middle of a file
can be treated as an unsupported character (zero-width invisible characters)
. if you are sending a string to another node on the net,
or an unfamiliar app on your node,
consider the BOM-related values {0,FFFE#16, 0,FFFF#16} invalid:
remove them from everywhere but the beginning of the string .
. the use of this reserve for BOM implies
all these are non-numbers:
U+{00... 10}{FF,FE... FF,FF}


. values in 0,D800 #16 .... 0,DFFF #16
are specifically reserved for use with UTF-16,
and don't have any characters assigned to them.
. { 0,FF,FE#16, 0,FE,FF#16 } are not Unicode char's precisely to preserve
their usefulness of as a BOM (byte-order mark)
--. either value prepended to a char'stream
is also a hint that it's unicode;
though the BOM can also be followed by a "UTF-16" tag:
eg,Big-endian text labelled with UTF-16, with a BOM:
FE FF D8 08 DF 45 00 3D 00 52 ... ;
Little-endian text labelled with UTF-16, with a BOM:
FF FE 08 D8 45 DF 3D 00 52 00 ... .
. the tags { UTF-16BE"(big-endian), "UTF-16LE"(little-endian), }
can be used in place of the BOM;
-- if the BOM is not at the beginning of the stream,
its meaning changes to a [zero-width non-breaking space] .
[9.15:
. FDD0...FDEF #16 represent noncharacters.
Unpaired surrogates are invalid as well,
i.e. any value in D800 ... DBFF #16
not followed by a DC00 ... DFFF #16,
or any value in DC00 ... DFFF #16
not preceded by a D800 ... DBFF #16 .
]
how unicode characters are encoded in UTF-16



. for (values <= 10,FFFF#16):
value < 1,00,00#16 ?
value may be contained in a single 16-bit integer .
value in 1,0000#16 ... 10,FFFF#16 ?
value - 1,0000#16 ( 0,yyyy,yyyy,yyxx,xxxx,xxxx #2 )
is returned in 2 words:
word#1 = 1101,10yy,yyyy,yyyy #2
word#2 = 1101,11xx,xxxx,xxxx #2

encoding ISO 10646 as UTF-16(U <= 0x10FFFF):
U < 0x10000 ?
return U as a 16-bit unsigned integer .
else
Let U' = U - 0x10000.
-- assert U <= 010,FFFF#16, implying U' <= 0F,FFFF#16 (fitting in 20 bits)
word#1`= 0xD800 -- assert word#1 = 1101,10yy,yyyy,yyyy
word#2`= 0xDC00 -- assert word#2 = 1101,11xx,xxxx,xxxx
word#1`[10 low-order bits]`= [U']`[10 high-order bits]
word#2`[10 low-order bits]`= [U']`[10 low-order bits]
return (word#1, word#2) .
Graphically, steps 2 through 4 look like:
U' = yyyy,yyyy,yyxx,xxxx,xxxx
W1 = 1101,10yy,yyyy,yyyy
W2 = 1101,11xx,xxxx,xxxx
U+D800 ... U+DFFF = 1101,1xxx,xxxx,xxxx

decoding ISO 10646 UTF-16 (U):
. word#1 not in 0xD800 ... 0xDFFF ?
return word#1
word#1 not in 0xD800 ... 0xDBFF ?
return error pointer to the value of W1
word#2 null or not in 0xDC00 ... 0xDFFF?
return error pointer to the value of W1
else:
return (word#1`[10 low-order bits] & word#2`[10 low-order bits])
+ 0x10000
) .

Security Considerations
in UTF-16 may contain special characters,
such as the [object replacement character] (0xFFFC),
that might cause external processing,
depending on the interpretation of the processing program
and the availability of an external data stream .
This external processing may have side-effects
that allow the sender of a message to attack the receiving system.

Implementors of UTF-16 need to consider
the security aspects of how they handle illegal UTF-16 sequences
(that is, sequences involving surrogate pairs
that have illegal values or unpaired surrogates).
It is conceivable that in some circumstances
an attacker would be able to exploit an incautious UTF-16 parser
by sending it an octet sequence that is not permitted by the UTF-16 syntax,
causing it to behave in some anomalous fashion.



UTF-16 extends UCS-2 by using 2words;
but not in the same way that UCS-4 does .

. UTF-32 is incompatible with ASCII files;
because, they contain many nul bytes;
implying the strings cannot be manipulated by normal C string handling .
Therefore most UTF-16 systems such as Windows and Java
represent text objects such as program code with 8-bit encodings
(ASCII, ISO-8859-1, or UTF-8), not UTF-16.
This introduces a serious complication in programming
that is often overlooked by system designers:
many 8-bit encodings (in particular UTF-8)
can contain invalid sequences that cannot be translated to UTF-16
and thus the file can contain a superset of the valid data.
For instance a UTF-8 URL can name a location
that cannot correspond to a file on the system,
or two different files may compare identical,
or reading and writing a file can change it.
One of the few counterexamples of a UTF-16 file is the "strings" file
used by Mac OS 10.3+ applications
for lookup of internationalized versions of messages,
these default to UTF-16
and "(files encoded using UTF-8 are not guaranteed to work.
When in doubt, encode the file using UTF-16).
Oddly enough, OSX is not a UTF-16 system.



ÒUnicodeÓ was originally BMP (U+0000 ... U+FFFF
-- Basic Multilingual Plane).
When it became clear that more than 64k characters would be needed,
Unicode was turned into a sort of 21-bit character set
range U-0000,0000 ... U-0010,FFFF .
The 2*1024 surrogate characters (U+D800 ... U+DFFF)
were introduced into the BMP to allow
1024*1024 non-BMP characters to be represented as
a sequence of two 16-bit surrogate characters.
This way UTF-16 was born,
which represents the extended Ò21-bitÓ Unicode
in a way backwards compatible with UCS-2.
The term UTF-32 was introduced in Unicode to describe
a 4-byte encoding of the extended Ò21-bitÓ Unicode.
. UTF-32 is the exact same thing as UCS-4,
except that by definition
UTF-32 is never used to represent characters above U-0010FFFF,
while UCS-4 can cover all 231 code positions up to U-7FFFFFFF.
The ISO 10646 working group has agreed to modify their standard to exclude
code positions beyond U-0010,FFFF,
in order to turn the new UCS-4 and UTF-32 into practically the same thing.




. some phrases can be expressed in more than one way in ISO 10646/Unicode.
For example, some accented characters can be represented as a single character
(with the accent) and also as a set of characters
(e.g., the base character plus a separate composing accent).
These two forms may appear identical.
There's also a zero-width space
with the result that apparently-similar items are considered different.
Beware of situations where such hidden text could interfere with the program.
This is an issue that in general is hard to solve;
most programs don't have such tight control over the clients
that they know completely how a particular sequence will be displayed
(since this depends on the client's font, display characteristics, locale, ...).

9.14:


In UTF-8, characters from the range U+00,00 ... U+10,FF,FF
(the UTF-16 accessible range)
are encoded using sequences of 1 to 4 octets.
table for converting UTF-32 to UTF-8:
UTF-32 range (hex.) UTF-8 octet sequence (binary)
00... 7F 0xxxxxxx
80... 07,FF 110xxxxx 10xxxxxx
08,00... 0,FF,FF 1110xxxx 10xxxxxx 10xxxxxx
01,00,00... 1F,FF,FF 11110xxx 10xxxxxx 10xxxxxx 10xxxxxx



C0#16 = 1100,0000#2
C1#16 = 1100,0001#2
F5#16 = 1111,0101#2
FF#16 = 1111,1111#2
D8,00 ... DF,FF -- illegal: control codes used by UTF-16:
. do UTF-16 -> UTF-32 -> UTF-8 .
This contrasts with CESU-8 [CESU-8],
which is a UTF-8-like encoding
that is not meant for use on the Internet.
CESU-8 operates similarly to UTF-8 but encodes the UTF-16 code values
(16-bit quantities) instead of the character number (code point).
This leads to different results for character numbers above 0xFFFF;
the CESU-8 encoding of those characters is NOT valid UTF-8.

[9.15:]
The definition of UTF-8 prohibits encoding character numbers between
U+, which are reserved for use with the UTF-16
encoding form (as surrogate pairs) and do not directly represent
characters. When encoding in UTF-8 from UTF-16 data, it is necessary
to first decode the UTF-16 data to obtain character numbers, which
are then encoded in UTF-8 as described above.
. thus, it is easy to convert to utf-8;
it is considerably less simple, however,
to validate that a utf-8 code was converted correctly;
. the code positions U+D800 to U+DFFF (UTF-16 surrogates)
as well as U+FFFE and U+FFFF
must not occur in normal UTF-8 or UCS-4 data.
(binary view of illegal chars)
U+D800 1101,1000,0000,0000
U+DFFF 1101,1111,1111,1111
U+FFFE 1111,1111,1111,1110
U+FFFF 1111,1111,1111,1111
. for safety reasons, UTF-8 decoders should treat them like
malformed or over-long sequences .

. the table above says this like so:
. say the 2..4 bytes have bits named bit#1 ... bit#32:
and bit#{ 1, 2 }  ?
assert bit#3 = 0, and byte#2 starts with 10.base2;
bit#{ 4 ... 8} & bit#{ 11 .. 16} --[ should be in range 0080 ... 07FF ]
< 80.base16 ? raise illegal.coding.error
else: and bit#{ 1, 2, 3 } ?
assert bit#4 = 0, and byte#{2,3} starts with 10.base2;
bit#{ 5 ... 8} & bit#{ 11 .. 16} & bit#{ 19 ... 24 }
--[should be in range 0800 ... FFFF ]
< 800.base16 ? raise illegal.coding.error
else: and bit#{ 1, 2, 3, 4} ?
assert bit#5 = 0, and byte#{2,3,4} starts with 10.base2;
bit#{ 6 ... 8} & bit#{ 11 .. 16} & bit#{ 19 ... 24 } & bit#{ 27 ... 32 }
--[should be in range 1,0000 ... 1F,FFFF ]
< 1,0000.base16 ? raise illegal.coding.error


. among a list of desiderata for any such encoding,
is the ability to synchronize a byte stream picked up mid-run,
with less that one character being consumed before synchronization.
. The model for multibyte processing has it that
ASCII does not occur anywhere in a multibyte encoding.
There should be no ASCII code values for any part of
a UTF representation of a character that was not in the
ASCII character set in the UCS representation of the character.
Historical file systems disallow the null byte and the ASCII slash character
as a part of the file name

1) zero the 4 octets (bytes) of the UCS-4 character
2) Determine which bits encode the character value
from the number of octets in the sequence
and the second column of the table above (the bits marked x).
3) Distribute the bits from the sequence to the UCS-4 character,
first the lower-order bits from the last octet of the sequence and
proceeding to the left until no x bits are left.
If the UTF-8 sequence is no more than three octets long,
decoding can proceed directly to UCS-2.




. UCS (Universal Character Set) is defined by ISO/IEC 10646
as having multiple octets (bytes) .
. UTF-8 (UCS transformation format -- 8bit)
is a way of staying compatable with single-byte ASCII
by using a 1...4-byte variable-length for describing
the same character set as the 4-byte UCS .


. CESU-8 (8-bit Compatibility Encoding Scheme for UTF-16)
is intended for internal use within systems processing Unicode
in order to provide an ASCII-compatible 8-bit encoding
that is similar to UTF-8 but preserves UTF-16 binary collation.
It is not intended nor recommended as an encoding used for open information exchange.
CESU-8 Bit Distribution
UTF-16 Code byte#1 byte#2 byte#3
0000,0000,0xxx,xxxx 0xxxxxxx
0000,0yyy,yyxx,xxxx 110yyyyy 10xxxxxx
zzzz,yyyy,yyxx,xxxx 1110zzzz 10yyyyyy 10xxxxxx

important features of this encoding form:
The CESU-8 representation of characters on the Basic Multilingual Plane (BMP)
is identical to the representation of these characters in UTF-8.
Only the representation of supplementary characters differs.
Only the six-byte form of supplementary characters is legal in CESU-8;
the four-byte UTF-8 style supplementary character sequence is illegal.
A binary collation of data encoded in CESU-8
is identical to the binary collation of the same data encoded in UTF-16.
As a very small percentage of characters in a typical data stream
are expected to be supplementary characters,
there is a strong possibility that CESU-8 data may be misinterpreted as UTF-8.
Therefore,
all use of CESU-8 outside closed implementations is strongly discouraged,
such as the emittance of CESU-8 in output files,
markup language or other open transmission forms.

converting {binary, hex}:
1000 8
1001 9
1010 10 A
1011 11 B
1100 12 C
1101 13 D
1110 14 E
1111 15 F

. for more examples, see wikipedia:





(binary view of illegal chars)
U+D800 ... U+DFFF = 1101,1xxx,xxxx,xxxx
these are for the 2 words in UTF-16:
word#1 = 1101,10yy,yyyy,yyyy
word#2 = 1101,11xx,xxxx,xxxx

U+FFFE 1111,1111,1111,1110
U+FFFF 1111,1111,1111,1111


todo:
see Unicode Technical Report #36, Unicode Security Considerations,
and Unicode Technical Standard #39, Unicode Security Mechanisms.

groovy scriptifies java`vm

adda/groovy scriptifies java`vm:
. pleac (Programming Language Examples Alike Cookbook)
after noticing that only 3 langs are finished,
I was wondering what groovy was about .
. groovy's birth comes from the same place as nu
which wants a lisp taylor-made for mac:
groovy scriptifies the java.vm
. there are other dynamic lang's for java.vm,
but they are bolt-on's;
eg, integration means it still likes such java verbosities as:
System.out.println(it) .
. the whole java thing is obviated by .net's
superior way of negotiating between security and freedom .
. byte code is machine code, low level and difficult to analyze,
so they did things like regulate the use of pointers
when what they needed to do was
just let a trusted compiler do the compiling,
it's at this high level where the client and server
can talk about capabilities,
where even c and its pointers become very safe
(the unit may be more likely to fail,
but it won't be spying, infecting, etc) .


advanced lang's do type inferencing

Operations on algebraic data types can be defined by using pattern matching
[this is, at least in their example,
the same as being able to program using the same code math does:
Tree.type = { variant? (Empty: null, Leaf: Int, Node: (l.Tree, r.Tree) };
depth(x.tree).int`=
{ return x`variant ?
(empty: 0
, leaf: 1
, others: 1 +max(depth x`left, depth x`right)
)} .
. this is a somewhat higher level than would be done in ada,
where you'd have to spell out
how you would be determining what variant a subtree was,
eg: empty(x.tree).truth`= '(return x=nil)
] .

preventing death of a language

10.5: adda/ada/preventing death:
they must mean that the foundational req's of the lang
are precluding modernization .
. one dimension of death prevention
is ensuring that there are tools that can automate
the translation of the current lang'
to any other lang' chosen as a future replacement .
. the other problem is how to make it easy for
the transition of language tools:
these tools read the lang'
and will be broken if the lang' changes .
. one solution is to use the mono system,
where the lang' of your choice is translated to a
high-level universal lang', or cil (common intermediate lang') .
. however, as was seen in the mono spec's,
designing a high-level universal lang is not easy:
there have have been several instances of
being unable to express some feature in terms of the cil .

bitc

10.4: web.adda/bitc/validating c as assembler code:

. reviewing the progress of gnu`hurd,
hurd/ng is referencing coyote who is working on bitc,
whose mailing list seems to be dwindling:

. it's got some interesting problems in 2005:

. recent bits:
Jonathan S. Shapiro Apr 7 2009:
. several people have asked what all of this means for Coyotos.
Active work on Coyotos stopped several months ago,
and is unlikely to resume.
I am debating whether to re-license it under BSD,
but other than that, I have no current plans to continue the Coyotos work.
Getitng BitC v1 done is already pushing the limits of what is feasible
pretty severely.
Sat Apr 25 13:15:24 EDT 2009:
We looked at C-- early on and decided not to go that way.
C-- has come a long way since then,
but the time for that option has passed.
Shapiro Feb 10 2009
At a certain point the complexity of the compiler got big enough
that Python was no longer the right tool.
We went to C++ rather than C because we wanted to use smart pointers.
In hindsight, we should have stuck with C.
2008.04 paper on bitc`origins:

what we didn't know then:
It is possible to program in something else (typically the prover)
and treat a small subset of a particular C implementation
as a well-defined assembly language,
as the L4.verified project has since done
Gerwin Klein, Michael Norrish, Kevin Elphinstone and Gernot Heiser.
``Verifying a High-Performance Micro-Kernel.''
7th Annual High-Confidence Software and Systems Conference,
Baltimore, MD, USA, May, 2007

. whatever its merits, ada is a dying language ...
it does not effectively exploit the advances in programming language theory
that have been made over the last two decades.


In ML, the use of state in the language is very carefully constrained to
simplify the core language semantics.
When state is introduced generally,
the language is suddenly forced to adopt a rich, first-class semantics
of locations into both the core semantics
and the core type system.
When let-polymorphism is present, adding core mutability
threatens the ability of the type inference engine
to generate principal types.
We wanted type inference, because Shapiro had witnessed
an unending stream of examples in UNIX
where failures to keep types synchronized across a code base led to errors,
and because
useable abstraction is hard to get in this class of language
without both type variables and type inference.
Being blissfully ignorant (at least when we started) of formal type theory,
all of this looked hard but straightforward,
which describes what kernel researchers do pretty much all the time:
navigate hard engineering compromises.
In fact, we soon learned that nobody had ever discovered
a sound and complete type system incorporating at the same time
both polymorphism and general mutability

Because of its preponderence for heap allocation,
extracting any sort of decent performance from an ML program
requires a level of optimization that is well beyond aggressive.
We needed a language that could preserve the illusion that
``what you see is what you get.''
This, among other issues, drove us to choose
eager rather than lazy evaluation.
object-oriented features actively got in the way of
understanding what was going on
however,
We needed the operator ``+'' to operate over arbitrary integer types.
Haskell presented a ready-made solution: type classes.
These simultaneously allowed us to generalize operators
and introduce a form of overloading into the language.
But type classes raise a problem that we will come back to later.
They introduce overloading and matching ambiguities that need to be addressed:
given two valid choices of specialization, which to choose?
In consequence, they have an unfortunate tendancy to break
separate compilation schemes.
Another issue with type classes is that the major implementations
all violate our code transparency objective.
The dictionary-based implementation technique
is not well-suited to languages having value types of multiple sizes;
we wanted an implementation that operated more in the style of C++ templates
-- not least because of the importance of linkage compatibility with C.
This would turn out to be the most problematic feature of the language.


In C, it is possible to have simultaneously a pointer to constant X
and a pointer to X,
both of which reference the same location.
This means that the compiler must be conservative when procedure calls are made.
In general, it cannot assume that supposedly constant objects
are unable to change.
In the interests of optimization, the ANSI C standard [1]
actually permits the compiler to make exactly this assumption.
Since there is no way for a C programmer to check whether
they have complied with the expectation of the compiler,
this is an invitation to error.
Since the result of computation depends on the
optimization decisions of particular language implementations,
bugs of this sort cannot be reliably eliminated through testing.
In BitC,
we decided very early to implement the notion of
immutability rather then constantness.
A BitC location that is declared to have immutable type
cannot be modified through [/]any reference.
In C, the ``const'' in const char is a type qualifier that can be stripped away.
In BitC it is an integral part of the type.
Actually, there wasn't any const type constructor in early BitC.
Variables and fields were constant unless declared mutable.

10.5:

The problems with module systems in stateful languages
are all about global variable initialization order.
. two language features that create problems for initialization order:
external declarations and assignment.
External declarations intentionally allow global identifiers
to be used before they are defined in ways that cannot be checked
when modules are compiled separately.
Assignment can cause initialized values to change between uses.
This either leads to a much finer dependency ordering on initializers
or to throwing up your hands and leaving ordering of effects during initialization undefined.
That may be type safe, but you get no guarantee about
what values global variables may hold when main() begins to run.
From a verification perspective this is problematic.
It is also makes the operation of a macro system
(which we intend to add in the future) undefined.
Well-formed programs invariably satisfy an implicit
lattice-structured dependency relationship for their initializers
(or at least don't get caught violating one).
The problem is that the ordering built by the compiler
is dictated by computational dependency,
while the organization of the program
required for manageability (the module relationships)
is dictated by conceptual relationships that exist in the minds of the developer.
The problem of initialization order is to satisfy both constraints simultaneously.

In BitC, we solved the initialization ordering problem
by declaring that interfaces are initialized first according to
the lattice defined by their import dependencies.
Within an interface, initialization proceeds from top to bottom,
and use of undefined forward references is prohibited.
It is source units of compilation that present the problem.

A BitC interface can declare a procedure that is implemented by
some exporting source unit of compilation.
In the absence of this feature,
we could declare that source units got initialized last in unspecified order.
Because source units can only export their identifiers through interfaces,
there cannot be further ordering dependencies
once the interface units have initialized in a defined order.

In the presence of export, this doesn't quite work.
What we do instead is to require that
any definition that is exported by a source unit
may rely (transitively) only on those symbols
that were in scope at the point of declaration in the interface.
The provided definition can rely on
other procedures and variables in the source unit,
and initialization proceeds as if all of those procedures and variables
had been temporarily copied into the interface unit of compilation.

But what about assignment and side effects?
And what if some of the procedures executed during initialization
get run multiple times?

9.2 Initialization vs. State

. permitting assignment during initialization is problematic.
Empirically, it isn't enough to require that
initializers be designed sensibly by the programmer
-- in the presence of shared libraries this requirement is nearly unachievable,
and the problem becomes more challenging in a higher-order programming language.
We cannot preclude the use of set! in initializers altogether.
This is too strong; it would prevent any occurrence of set!,
even if the containing procedure is not called at initialization time.
And strictly speaking, we can allow assignments in initializers
as long as the results of those assignments do not escape.

The position taken in BitC is that initializers must be ``pure,''
meaning that they may not modify any globally reachable values.
Implementing this forced us, with considerable hesitation,
to adopt an effect type system (Section 10).
10.5: adda/bitc/verifiable and modern systems prog' lang:
. after reading about the origins and req's of bitc
I was worried about the job ahead for designing adda .
. the storm shelter is to be found in modularity:
to be safe,
the system need only confine systems prog'ing to a module;
and within that module the system doesn't have to be safe:
it's ok if a module fails
so long as the failure doesn't bedevil other modules .
. for systems prog'ing with adda
we need to see how adda maps directly to c
while still staying true to the adda syntax .
efficiency:
. one paper points out why efficiency matters:
systems prog'ing is responsible for the energy use of data centers,
and that energy comes mostly in the form of cooling .
. the more cycles we use, the greater that ac bill .
. a major waste of energy is copying data that could be shared,
and there are 2 routes:
the complicated way is to try providing safe sharing;
while the easy way is to let systems prog'ing
happen in a separate, background process,
where any freeze-up's won't bedevil the safe parts .
[10.10: ie,
the most important thing for prototyping
is to help the user be an effective app'programmer
where worrying about efficiency can happen later . ]


10.5: bk.adda/Why Systems Programmers Still Use C:
. Singularity may obviate the cap'based coyote.os
. the Singularity project is probably the most serious challenge
to the current Coyotos work in the secure embedded system space.
There are some denial of resource issues
that are inherent in the Singularity communications layer.
These are fixable, and we gave serious thought to
replacing the Coyotos system with a structurally similar system
built on Singularity-like foundations.
In the commercial Coyotos effort,
we reluctantly concluded that the schedule risk
to our current commitments was too high,
but we think that there is an interesting research challenge here:
enhance the linear type approach of Singularity messages
with complete storage accountability during message exchange.
See if a system can be successfully structured
using language based mechanisms when abandoning the assumption
that there is an infinite pool of storage .
. if linear types prove to be a human-manageable mechanism
for handling interprocess communication,
it may really be true that
the era of hardware-based isolation is over .
Most of the performance unpredictability issues of garbage collection
become irrelevant if collection occurs over a small heap.
By increasing messaging performance,
Singularity permits applications to be split into
much smaller, independently collected domains.
Robustness is simultaneously improved.


Swaroop Sridhar, Jonathan S. Shapiro, Scott F. Smith



10.6: todo.adda/advanced typing systems:
. type systems of ml and haskell origins?
and see downloaded papers .



Sedgewick` Algorithms


10.5:
adda/parse.tree:
. a parse tree is the usual name for what I called an etree (expression tree)

adda/forest:
. a forest is a tree that is not binary;
[10.9:
eg, in the universe of acyclic graphs
lists have only 2 edges, trees 3, and forests > 3 .
. forests can be impl'd with trees
by having one edge leading to the next node extension,
rather than a 2nd child . ]
any node in a forest:
. if a tree has 2 way edges
then any node can be root
but it becomes a forest .

10.6: adda/breadth-first search:
. breadth-first search is done by a
non-recursive pre-order traversal
but where the algorithm replaces the usual stack access
with a queue .