| Sticky Revision: |
r5008@brainchild: ctl | 2008-10-24 16:50:07 -0400 irrelevant old changes
r2841@brainchild: ctl | 2007-05-31 16:36:40 -0400 merge conftest changes into trunk
make nonce explicit
s/stream_nonce/series_nonce/
change syntax of hash and uia principals.
move basic_test into top lib directory.
Un-revert the library move, and incorporate the needed bits from my branch into the trunk. This should work if you re-configure (from the top level) and re-install.
revert -r2498:2502 -- broke the install
Move pylib files needed by both alpaca and uianet/router into a separate top-level directory.
Resolve semantic merge conflicts (at least, some of them). UIAnet now builds properly, and calc.py's test suite runs again.
a couple of additions
updated comprehensive todo list.
implement one-time-authenticator authority for alpaca. current only used to implement ping-of-death in llamalab.
Implemented a model version of planetlab. Supported operation: - contribute resources (disk) to the node - principal a grants quota to principal b - principal creates a "sliver" (virtual machine) on the node - sliver requests to grow its resource (disk) usage (modeled by a request by the principal)
Simplistic implementation of a quota network.
fix error message handling.
move alpaca doc tree into its own trunk dir so that people don't have to download 16MB of PDFs and latex.
move alpaca source tree into the uia trunk
change name to "sandbox" authority
implement vx wrapper (yet untested)
Fix tiny test suite bug in sexp.py. Attempt and fail to get py.test to work on pylib.
Move directory name pcp->alpaca
Change name PCP->Alpaca.
llama photos
Another diagram, everything tidied up; this is the version I'm going to present.
Many comments incorporated; some diagrams reworked.
Notes from Max I have yet to incorporate usefully.
Another totally reworked draft.
some related works, some random notes.
spelling errors
rtm comment
expand the lemma example considerably --- better?
remove DRAFT footer
Write a short, not very good summary. In submittable state, will submit a version asap.
Try to address some of frans's other comments about confusing jargon
clean up overview figure a bit.
kill some more XXXes
I'm an idiot, Jacob caught me citing where I should be reffing
fill in a bit of future work section
fix accumulated bugs pointed out by frans
add paragraph about uia implementation
overhaul sections 3.3 and 3.4 as per suggestions of frans.
fix figure and table captions.
frans and robert's comments on abstract, intro, background
I am almost a paper.
all citations should be valid now
Remove motivation (how apt)
overwrite with figure from talk
delete old figure
It is a whole draft again after being gutted. 12 pages, so room to expand. Need thorough massaging of structure and XXXs tomorrow.
Forgot to check in new pulled-out background section.
insert comments from frans. deal in morning.
unbroke the build
tweak references.
Finish basic PKI section. What remains is an unknown amount of space devoted to the advanced tricks section.
reorganize names
reorganize implementation into future work, fill out serialization
api description
Authority section
forgot to check in this image before.
A checkpoint. Everything is indeed still a mess.
checkpoint (submitted abstract)
version presented on 9-12
simple demo
new draft abstract
fix __future__ in wrong place; add small demo harness add some random notes; set svn:ignore properties
change directory name to contain date of presentation.
frans's suggestion
comment from Russ
alpaca pictures
"final" version
almost completely filled out --- probably 3 hours worth of material :(
oops, that wasn't the right file.
actually include text
pdos presentation draft
caching to improve performance a bit...
just some notes to myself on linear logic.
use filename instead of __main__
a self-contained test framework minimally compatible with py.test
handle newer version of pyparsing, with memoization changes I suggested to maintainer
refactoring, performance improvements, expose interfaces
further reorg
clean up old irrelevant version
package reorganization and some resultant renames and bugfixes
paths change
reorganize and refactor tests
updated to use new pkcs1 framework
massive overhaul of pkcs1 code for spec compatibility
check in skeleton modifications
rename
nsdi branch
needed an __init__.py
update certificate chain and fix some minor bugs
after long travails, generated a single precious certificate chain.
fix x509 signature computation
x509 signature checking
x509 encoding/decoding
expanded ca endorsement theorem, sign using hash
readme, another related doc on proof compression, some tools
ASN.1, DER, PKCS1 implemented. Many related changes.
various changes to support named integration.
various performance tuning, bug fixes, etc.
proof compression / serialization --- only gimpy version works.
streamlined api
untested eid delegation lemmas
fixup fresh variables
kill let command
streamline some theorem code.
eid principals with rsa signatures
encapsulate into principal classes
rsa proof
write lemmas and contexts for prover to support hash principals
logic axioms
tidy up interfaces again.
clean up lemmas and last usage, refactoring mostly done.
tabular authorities as instances, not classes.
get witnesses provisionally working again
bring principals into theorem land
encapsulate theorems as a statement with a proof.
proof combinator
fix subtle alpha-substitution/free-variable bugs.
replace all uses of 'apply' with new magic 'deduce', and fix consequent bugs.
new magic deducer, thank god that's working.
rsa key proving works.
importing authorities
function authorities, general refactoring of authorities.
math and encoding for integers
create integer constants
streamline parser. sadly, tests with psyco indicate that psyco is broken.
fix transition-related bugs, clean up code.
test cases
rewrite case->union, expression, proof classes.
finish tree and test-case reorg.
more tree reorg
reorganize tree
reorganize tree
reorganize package
test suite tests right thing
swap names of beta-reduce and beta-abstract to be consistent with others.
reduce proof-generating kludginess.
main proof for hash principals compiles and checks out.
prove delegation theorems.
implement substitute and apply
keep track of lemmas.
proof inference in principals' contexts.
fix base64 encoding implement several authorities refactor proof command interpreter using decorator new claim checker
names
equals and says
modify sandbox branch
new sandbox branch
many changes dealing with level inference for contexts. kind of kludgey.
refactor some expression-munging code out of proof.py.
OK, level solving in proof inference seems to work, albeit in a minimal way! What a nice way to start the week.
new beta-reduction code works well now.
reworking beta-reduction search, taking a break for food.
new beta reduction checker, hopefully also better.
checkpoint last night's proof inference code.
partial proof inference engine.
more prover automation is good.
more believable level code
generalize level structure for proof inference
some definitions for data, skeletal uia context for reference only
hit a darn hairy snag.
various logic definitions
some very difficult manual proofs
pretty up the test suite.
proofs work again, with fancy generic types and all. 17 proofs in test suite all work again.
pull implicit levels from context
first step in reformulating parser for context. also some cleanup.
midway through restructuring more robust proof code
another checkpoint with broken proofs
more sophisticated generics support in parser
intermediate check-in --- non-working state, but there's just too many changes to kep everything in working copy anymore.
more related work
many bug fixes, progress on the message verification front, but unexpected badness on the paradox-avoiding front.
empty file needed to find modules
substitute constant
renaming of modules
rename directory
keep old branch around in handy location for now.
trash old-old files
various other related works I've been poring over
a whole bunch of stuff I've failed to check in before...
some hastily scribbled notes
notes dump
checkpoint, postmortem
sad, sad slides
pull in skeleton from previous pdos presentation
submitted PDF
submitted version
abstract
minor related and summary tweaks
finished pass over examples
frans nits
worked up through hashes.
footnote
work over x.509 and dnssec sections.
let's move around cut blocks and see what needs to be salvaged.
apply robert's comments
some minor wording and formatting clarifications.
hack and slash based on frans comments. improved, but still doesn't flow with the rest.
make expression notation less bulky. much more pleasant to look at now!
cargo-cult latex squeezing
rule 1: fix the easy things first
all sorts of changes, formatting, also fixes to frans's comments to first 3 sections.
one more edit.
streamline interface section somewhat. wording tweaked, subsections reorganized to reduce redundancy, figures trimmed. downside: the actual content of proofs remains put off to the next section.
make figure more consistent with text
tweak 3.0
fix figure labels
minor tweaks to wording here and there. edit figure to be more complete but more complex.
tweak intro a bit more; perhaps more comprehensible now.
improve accuracy of intro.
Streamlining intro
latex-style quotes, fix some citation locations
clarify policy-mechanism in intro, somewhat clarify role of bob. (robert's comments)
snip down intro section. add more citations.
various related works, for reference
actually check in the new section
motivation section, first draft. very long.
huge quantities of tweaking. fits under 6 pages! (6.5 -> 6 achieved by cheating and setting tiny margins)
rewrite intro to account for robert's comments.
jvm and clr refs
I'm a "real" "paper" now. (summary section) Now all that's needed is a complete reorganization.
related work section.
some bibliography
i.e., e.g.,
work out pgp example. start bibliography.
dnssec and sdsi
partway through examples fleshing-out
further tweaks, formatting, wording --- no major reorg.
reorganize somewhat; try to address round 1 of frans's comments.
start in a tiny bit of implementation section (this may be redundant)
fill out rest of interface section
formatting change so it compiles
convert rest to latex
use latex instead of rest
ReST modifications
checkpoint of a draft
basic outline of certificate subsystem.
kludge libtool to statically link libuip
hack in some goo to barely interface with UIP transport.
a bunch of half-working uipsock interface code --- need to completely rework this.
some goop to prove UIP-style self-certifying messages. uses RSA instead of DSA --- don't want to have to hash messages yet! this goop is really kludgey. this codebase wants an overhaul badly.
dsa support
skeleton of uip support
various prep for restructuring, integration
some more todo
Throw together blecherous example application.
extensive changes -- encapsulate and refactor all message proving functionality.
a whole mess of edits in order to refactor certificates, in preparation for incorporating into a test application. not in a working state!
now checking messages with real RSA keys. keys have to be very long (and hence slow to generate) because we're not doing any message hashing. (This is intentional, since the whole point is to bootstrap that stuff.)
add hooks to verify messages using the module entry point
wrote the two-line toplevel stub that would be called by an external module. still todo: write documentation for this rubbish.
proofs can be marshaled and unmarshaled
incorporate marshaling/unmarshaling into expression code directly. should this really go in another file? it's not part of the TCB.
we now have a proof proving itself to a verifier.
new pretty printer uses proof flattening code.
prover/verifier interface, mark N. pretty printing works, but need to hook it up to marshal/unmarshal.
get rid of test file
test commit email
test commit email
test commit email
remove test
test commit email
test commit email
test commit email
test commit email
make tests more consistent prepare some notes about proofs
test
test
test
test
test commit mail
test commit
begin framework for real RSA. (NYI)
break out witness axiom into separate module
add RSA snake oil --- for testing purposes only!
fix representation test it in message.py
expose the "representation" function
both instance axioms are now "key says something"
fix parser to accept no-argument functions, e.g. constants.
use s-expressions for representation. hopefully this will be easier to incorporate into the logic.
first stab at representation code. extant problems: - doesn't scrub symbols --- should only allow conservative values - let's dump this syntax and do s-exps. so much nicer.
clean up code a little bit more
message proof much simplified by use of generalized infer. next step: extend proof backwards
since the new implementation is also python, this is a better name.
great, generalized substitution and inference seems to work.
further prepare infrastructure for real axioms
new parser implementation. a bit ugly, but shorter than the old one...
fit in the generalized inferencer; start to build up axioms (NYI)
fix subtle substitution bug
converted and-elimination-right proof to brave new world.
proof infrastructure
first module of brave new implementation --- disturbingly similar to old implementation.
move all this unwieldy python stuff into its own directoy
yet another half-assed broken checkpoint
checkpoint --- nothing works at this point
large portion of a single message proof
logically unsound changes to make says work. this is only for testing purposes! burn it all down and start from scratch for final draft.
checkpoint of a couple random changes -- about to restructure entirely
intermediate state I used to demo to Frans.
intermediate state
questionable substitution code. when is the type checking going to come in?
oops, forgot to check in primary domain file
baby's first proof!
lots of code to fill out Domain class --- not yet working
implemented expression comparison
fix parsing bug --- I really should refactor the "parsing position" code out.
refactor parsing code; implement semantics implement substitutions.
some initial parsing code
framework
| Maintained by PDOS | ViewVC Help |
| Powered by ViewVC 1.0.3 |
Directory Listing