arguing the security properties of xsnap (XS, SES, JS) #7858

dckc · 2021-01-20T15:14:08Z

dckc
Jan 20, 2021
Collaborator

dckc · 2021-01-20T15:42:47Z

dckc
Jan 20, 2021
Collaborator Author

Hardware support? MPX in Intel Skylake

From What is memory safety? - The PL Enthusiast:

Pointers as capabilities

The definition I prefer, which I’ll now present, is inspired by Santosh Nagarakatte‘s work (done with several collaborators) on SoftBound, an approach for enforcing memory safety in C programs (which has inspired Intel hardware support, coming soon).

Intel MPX - Wikipedia citing "Intel Software Development Emulator". Intel. 2012-06-15:

Intel MPX was introduced as part of the Skylake microarchitecture.

grep -i mpx /proc/cpuinfo shows mpx, suggesting it's on my machine.

Intel® Memory Protection Extensions (Intel® MPX) support in the GNU toolchain says it's deprecated, and Wikipedia goes on to say "In practice, there have been too many flaws discovered in the design for it to be useful, and support has been deprecated or removed from most compilers and operating systems." But it still looks interesting, to me. Wikipedia doesn't note the connection to capabilities. I wonder how similar it is to CHERI.

0 replies

dckc · 2021-01-20T16:09:56Z

dckc
Jan 20, 2021
Collaborator Author

Executable: 1.5M

2.7M for debug

agoric-sdk/packages/xsnap$ ls -lsh build/bin/lin/*/xsnap
2.7M -rwxrwxr-x 1 connolly connolly 2.7M Jan 23 20:03 build/bin/lin/debug/xsnap
1.5M -rwxrwxr-x 1 connolly connolly 1.5M Jan 23 20:03 build/bin/lin/release/xsnap

Compiled C: 2,084KB

agoric-sdk/packages/xsnap/build/tmp/lin/release/xsnap$ ls -sh *.o
8.0K xsAll.o         96K xsDataView.o    36K xsJSON.o       36K xsObject.o      28K xsScope.o
 60K xsAPI.o        120K xsDate.o        60K xsLexical.o    12K xsPlatforms.o   16K xsScript.o
8.0K xsArguments.o  8.0K xsDebug.o       48K xsMapSet.o    4.0K xsProfile.o     68K xsSnapshot.o
 80K xsArray.o       16K xsDefaults.o    20K xsMarshall.o   32K xsPromise.o    8.0K xsSourceMap.o
 60K xsAtomics.o     44K xsdtoa.o        24K xsMath.o       12K xsProperty.o    52K xsString.o
 64K xsBigInt.o      12K xsError.o       68K xsMemory.o     36K xsProxy.o       16K xsSymbol.o
4.0K xsBoolean.o     24K xsFunction.o    36K xsModule.o     32K xsRegExp.o     108K xsSyntaxical.o
 96K xsCode.o        24K xsGenerator.o   48K xsnap.o       292K xsre.o          60K xsTree.o
 48K xsCommon.o      24K xsGlobal.o      16K xsNumber.o     88K xsRun.o         32K xsType.o


agoric-sdk/packages/xsnap/build/tmp/lin/release/xsnap$ ls -s *.o >,siz
agoric-sdk/packages/xsnap/build/tmp/lin/release/xsnap$ python

Python 2.7.17 (default, Sep 30 2020, 13:38:04) 
>>> lines = open(',siz').readlines()
>>> sum([int(line.strip().split(None, 1)[0]) for line in lines if line.strip()])
2084

Dependencies: libc, libpthread only

The debug build also has some socket stuff but we no longer use that in production: #2216

agoric-sdk/packages/xsnap$ ldd build/bin/lin/release/xsnap 
	linux-vdso.so.1 (0x00007ffe61391000)
	libm.so.6 => /lib/x86_64-linux-gnu/libm.so.6 (0x00007f57743c6000)
	libpthread.so.0 => /lib/x86_64-linux-gnu/libpthread.so.0 (0x00007f57741a7000)
	libc.so.6 => /lib/x86_64-linux-gnu/libc.so.6 (0x00007f5773db6000)
	/lib64/ld-linux-x86-64.so.2 (0x00007f5774ae5000)

agoric-sdk/packages/xsnap$ nm build/bin/lin/release/xsnap | grep 'U '
                 U acos@@GLIBC_2.2.5
                 U acosh@@GLIBC_2.2.5
                 U asin@@GLIBC_2.2.5
                 U asinh@@GLIBC_2.2.5
                 U atan2@@GLIBC_2.2.5
                 U atan@@GLIBC_2.2.5
                 U atanh@@GLIBC_2.2.5
                 U calloc@@GLIBC_2.2.5
                 U cbrt@@GLIBC_2.2.5
                 U cos@@GLIBC_2.2.5
                 U cosh@@GLIBC_2.2.5
                 U __ctype_tolower_loc@@GLIBC_2.3
                 U __errno_location@@GLIBC_2.2.5
                 U exit@@GLIBC_2.2.5
                 U exp@@GLIBC_2.2.5
                 U expm1@@GLIBC_2.2.5
                 U fclose@@GLIBC_2.2.5
                 U fdopen@@GLIBC_2.2.5
                 U feof@@GLIBC_2.2.5
                 U fflush@@GLIBC_2.2.5
                 U fgetc@@GLIBC_2.2.5
                 U floor@@GLIBC_2.2.5
                 U fmod@@GLIBC_2.2.5
                 U fopen@@GLIBC_2.2.5
                 U __fprintf_chk@@GLIBC_2.3.4
                 U fputc@@GLIBC_2.2.5
                 U fputs@@GLIBC_2.2.5
                 U fread@@GLIBC_2.2.5
                 U free@@GLIBC_2.2.5
                 U fwrite@@GLIBC_2.2.5
                 U gettimeofday@@GLIBC_2.2.5
                 U hypot@@GLIBC_2.2.5
                 U __isoc99_fscanf@@GLIBC_2.7
                 U __libc_start_main@@GLIBC_2.2.5
                 U localtime@@GLIBC_2.2.5
                 U log10@@GLIBC_2.2.5
                 U log1p@@GLIBC_2.2.5
                 U log2@@GLIBC_2.2.5
                 U log@@GLIBC_2.2.5
                 U __longjmp_chk@@GLIBC_2.11
                 U malloc@@GLIBC_2.2.5
                 U memcmp@@GLIBC_2.2.5
                 U __memcpy_chk@@GLIBC_2.3.4
                 U memcpy@@GLIBC_2.14
                 U memmove@@GLIBC_2.2.5
                 U memset@@GLIBC_2.2.5
                 U mktime@@GLIBC_2.2.5
                 U nearbyint@@GLIBC_2.2.5
                 U pow@@GLIBC_2.2.5
                 U __printf_chk@@GLIBC_2.3.4
                 U pthread_cond_destroy@@GLIBC_2.3.2
                 U pthread_cond_init@@GLIBC_2.3.2
                 U pthread_cond_signal@@GLIBC_2.3.2
                 U pthread_cond_timedwait@@GLIBC_2.3.2
                 U pthread_cond_wait@@GLIBC_2.3.2
                 U pthread_mutex_destroy@@GLIBC_2.2.5
                 U pthread_mutex_init@@GLIBC_2.2.5
                 U pthread_mutex_lock@@GLIBC_2.2.5
                 U pthread_mutex_unlock@@GLIBC_2.2.5
                 U pthread_self@@GLIBC_2.2.5
                 U puts@@GLIBC_2.2.5
                 U qsort@@GLIBC_2.2.5
                 U rand@@GLIBC_2.2.5
                 U realloc@@GLIBC_2.2.5
                 U __realpath_chk@@GLIBC_2.4
                 U round@@GLIBC_2.2.5
                 U _setjmp@@GLIBC_2.2.5
                 U sin@@GLIBC_2.2.5
                 U sinh@@GLIBC_2.2.5
                 U __snprintf_chk@@GLIBC_2.3.4
                 U __sprintf_chk@@GLIBC_2.3.4
                 U sqrt@@GLIBC_2.2.5
                 U __stack_chk_fail@@GLIBC_2.4
                 U __stpcpy_chk@@GLIBC_2.3.4
                 U strcat@@GLIBC_2.2.5
                 U strchr@@GLIBC_2.2.5
                 U strcmp@@GLIBC_2.2.5
                 U __strcpy_chk@@GLIBC_2.3.4
                 U strcpy@@GLIBC_2.2.5
                 U strerror@@GLIBC_2.2.5
                 U strlen@@GLIBC_2.2.5
                 U strncat@@GLIBC_2.2.5
                 U strncmp@@GLIBC_2.2.5
                 U strncpy@@GLIBC_2.2.5
                 U strrchr@@GLIBC_2.2.5
                 U strstr@@GLIBC_2.2.5
                 U strtol@@GLIBC_2.2.5
                 U tan@@GLIBC_2.2.5
                 U tanh@@GLIBC_2.2.5
                 U __vfprintf_chk@@GLIBC_2.3.4
                 U __vsnprintf_chk@@GLIBC_2.3.4

strcpy

I don't see any guarantee that strcpy in fxBuildModuleMap is memory-safe. TODO: check whether if (preparation && the->archive) is always false in xsnap.

0 replies

erights · 2021-01-20T17:46:50Z

erights
Jan 20, 2021
Maintainer

Good! Yes, please move to Agoric.

…

On Wed, Jan 20, 2021 at 7:14 AM Dan Connolly ***@***.***> wrote: @erights <https://github.com/erights> , you asked me how I'd go about this... the question has been rattling around in my head and it's starting to take shape... let me know if I should move this under the Agoric org. during this early brainstorming stage. ...

-- Cheers, --MarkM

0 replies

dckc · 2021-01-22T18:19:42Z

dckc
Jan 22, 2021
Collaborator Author

for reference, earlier discussions:

2016: Proof of security tc39/proposal-ses#4 SES Proof of security
2019: Chainmail info? #198 Chainmail info?

0 replies

dckc · 2021-01-24T04:57:43Z

dckc
Jan 24, 2021
Collaborator Author

splint looks somewhat promising... with a few annotations, it might be able to make a pretty good memory-safety argument.

The defaults seem incompatible with the current XS idioms, but perhaps that could be addressed easily:

moddable/xs/sources]$ splint +posixlib -I ../includes/ -I ../platforms/ xsDate.c
Splint 3.1.2 --- 02 Dec 2020

../platforms/xsPlatform.h:81:26: #error unknown compiler
  Preprocessing error. (Use -preproc to inhibit warning)
   In file included from xsCommon.h:41,
                 from xsAll.h:41,
                 from xsDate.c:38
xsAll.h:1942:85: Invalid character in macro parameter name
   In file included from xsDate.c:38
xsAll.h:1942:85: Parameter list for #define is not parseable
xsAll.h:1957:88: Invalid character in macro parameter name
...
*** Cannot continue.

found while looking for CCured via SO clue.

SAFECode

SAFECode: Enforcing Alias Analysis for Weakly Typed Languages
Dinakar Dhurjati, Sumant Kowshik, and Vikram Adve.
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2006

https://news.ycombinator.com/item?id=17143237

[1705.07354] The Meaning of Memory Safety

Checked C looks active

Checked C: Making C Safe by Extension - Microsoft Research
September 2018

https://github.com/Microsoft/checkedc 52d7a7f on Dec 18, 2020

https://github.com/Microsoft/checkedc-clang/releases 2020-07-31 2745f7d

0 replies

dckc · 2021-01-27T05:51:55Z

dckc
Jan 27, 2021
Collaborator Author

fuzzing

I played around with AFL tonight.
AFL: american fuzzy lop - a security-oriented fuzzer

This looks like the result of some fuzzing too:

SEGV at /xs/sources/xsBigInt.c:1182 · Issue #485 · Moddable-OpenSource/moddable

looking at other work by the reporter...
kvenux/capflow: Isabelle proof for CapFlow

and from there:
A Verified Capability-Based Model for Information Flow Security With Dynamic Policies

p.s. cf https://github.com/wasmerio/wasmer/tree/master/fuzz

0 replies

dckc · 2021-01-28T17:52:10Z

dckc
Jan 28, 2021
Collaborator Author

getters and setters vs. static analysis

The main difference between SES and SES_light is that SES supports getters/setters and SES_light does not because they are not amenable to the analysis methods we considered practical and ...

-- Automated Analysis of Security-Critical JavaScript APIs
found via A Taxonomy of Security Issues - Agoric

0 replies

erights · 2021-01-28T17:57:44Z

erights
Jan 28, 2021
Maintainer

Yes. And JS has changed even more since that article was written.

0 replies

dckc · 2021-02-01T23:01:01Z

dckc
Feb 1, 2021
Collaborator Author

to prevent escape from vat:

compile to WASM
seccomp

@erights wondered about in-vat mutual-suspicion boundaries:

zcf vs. the contract
liveSlots vs. running code
- non-determinism

p.s. browsing...

Formalizing the LLVM Intermediate Representation for Verified Program Transformations
esbmc/esbmc: The efficient SMT-based bounded model checker
static-analysis-engineering/CodeHawk-C: CodeHawk C Analyzer: sound static analysis of memory safety (undefined behavior)

setjmp / longjump

Support for setjmp / longjmp · Issue #2625 · rust-lang/rfcs

frama-C doesn't support it.

0 replies

dckc · 2021-02-02T17:57:17Z

dckc
Feb 2, 2021
Collaborator Author

esmbc -- Efficient model checking with CI techniques

This looks like a particularly good match for XS:

Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking

The project is active; the maintainers responded to an issue within a day: esbmc/esbmc#355 (comment)

Map2Check -- fuzzing and symbolic execution

esbmc contributors overlap with https://github.com/hbgit/Map2Check , which combines fuzzing and symbolic execution.

tried the release from late 2019; not promising:

~/opt/map2check$ ./map2check  --target-function fxBuildDate ~/projects/moddable/build/tmp/lin/debug/xst/xsDate.bc
Adopting z3 solver... 
Started Map2Check
std::bad_alloc

nesCheck -- good performance on subset of C

adding "embedded" to our search terms turns up other interesting work...

nesCheck is aimed at a constrained subset of C, but the results are interesting:

Through extensive evaluation benchmarks – both on specifically constructed programs and the standard TinyOS applications – we showed the effectiveness of nesCheck in enforcing memory protection while minimizing the runtime performance overhead (0.84% on energy, 5.3% on code size, up to 8.4% on performance, and 16.7% on RAM).
-- Midi et. a. 2017

0 replies

dckc · 2021-02-04T05:42:41Z

dckc
Feb 4, 2021
Collaborator Author

I'm experimenting with coverity scan: https://scan.coverity.com/projects/dckc-moddable?tab=overview

hmm... more involve than my first impression suggested.

0 replies

dckc · 2021-02-11T17:53:44Z

dckc
Feb 11, 2021
Collaborator Author

discovered https://github.com/google/oss-fuzz by way of https://twitter.com/LazyFishBarrel today

fuzzing/libFuzzerTutorial.md at master · google/fuzzing

Google Online Security Blog: Improving open source security during the Google summer internship program

0 replies

dckc · 2021-02-22T17:30:05Z

dckc
Feb 22, 2021
Collaborator Author

https://github.com/trailofbits/manticore , a Symbolic execution tool, can analyze WebAssembly . I wonder if analysis of XS compiled to WASM would be fruitful.

0 replies

dckc · 2021-03-02T20:13:14Z

dckc
Mar 2, 2021
Collaborator Author

tangentially related... (i.e. above the xsnap layer... or is it?)

@erights writes:

We need to introduce and document and maintain a careful distinction of the names of static direct hardeners. harden obviously but now also Far and for the moment Data are all in this category. Likely makeKind too though I have not looked lately.

We can add static amountMath and its static methods, or some of its static methods to that list.
When we write a static verifier for hardening, it must know about this category.

0 replies

dckc · 2021-03-02T22:35:53Z

dckc
Mar 2, 2021
Collaborator Author

Another fuzzing expert is working on XS! Go @rain6851 !

Moddable-OpenSource/moddable#580
thru
Moddable-OpenSource/moddable#587

cc @erights

0 replies

dckc · 2021-04-11T14:52:59Z

dckc
Apr 11, 2021
Collaborator Author

safety, metering via WASM?

Crazy idea? Kill two birds with one stone by compiling xsnap to WASM:

metering - reuse WASM metering from other mature blockchain work ( https://github.com/CosmWasm/cosmwasm ? )
fail-stop safety: if XS isn't memory safe, WASM should make it fail-stop
- caveat: is the WASM runtime memory safe? perhaps in safe rust? can we completely trust safety of rust?

cc @michaelfig @warner @erights @dtribble @kriskowal

0 replies

zmanian · 2021-04-11T18:31:58Z

zmanian
Apr 11, 2021

General information here

There are two dominant standalone WASM execution ecosystems. The BytecodeAlliance ecosystem and Wasmer ecosystem. Cosmwasm and Near protocol user Wasmer and Substrate uses the Bytecode Alliance ecosystem.
Both ecosystems have support for Go bindings and metering. Using wasmer might be slightly preferred because more reference code can be generated from cosmwasm.
AFAIK, wasmer 1.0 massively reduced the amount of unsafe rust in their code base. Wasmer is also extensively fuzz tested to ensure the single pass JIT isn't a source of sandbox escapes.

0 replies

dtribble · 2021-04-11T20:59:57Z

dtribble
Apr 11, 2021
Maintainer

safety, metering via WASM?

Crazy idea? Kill two birds with one stone by compiling xsnap to WASM:

metering

fail-stop safety: if XS isn't memory safe, WASM should make it fail-stop

We considered this option (ty Zaki for the detailed options).

WRT metering, that means that the actual metering costs now derive the the entire tool chain of compilation of C to WASM, and the presents as a mysterious mapping to user-specified code. It ensures that nothing escapes the metering, but it would also make it difficult to have select things with custom metering (e.g., if we wanted to charge fixed costs for some class of crypto operations to not penalize multisig).

WRT fail-stop memory-safety, we are already in position to have each vat run in a separate process, so WASM adds nothing there. It could conceivably provide stronger safety for multiple-vats within a single process, but for the cost of checking that taller tool chain, we could add other memory safety sanity checks.

I would like to see XS or something like it directly in Rust someday :).

0 replies

dckc · 2021-04-12T13:51:26Z

dckc
Apr 12, 2021
Collaborator Author

WRT metering, that means that the actual metering costs now derive the the entire tool chain of compilation of C to WASM,

Yes, I thought of that soon after I posted the idea. Any change at the C layer would change metering results.

0 replies

arguing the security properties of xsnap (XS, SES, JS) #7858

dckc Jan 20, 2021 Collaborator

Replies: 19 comments

dckc Jan 20, 2021 Collaborator Author

Hardware support? MPX in Intel Skylake

Pointers as capabilities

dckc Jan 20, 2021 Collaborator Author

Executable: 1.5M

Compiled C: 2,084KB

Dependencies: libc, libpthread only

strcpy

erights Jan 20, 2021 Maintainer

dckc Jan 22, 2021 Collaborator Author

dckc Jan 24, 2021 Collaborator Author

SAFECode

Checked C looks active

dckc Jan 27, 2021 Collaborator Author

fuzzing

dckc Jan 28, 2021 Collaborator Author

getters and setters vs. static analysis

erights Jan 28, 2021 Maintainer

dckc Feb 1, 2021 Collaborator Author

setjmp / longjump

dckc Feb 2, 2021 Collaborator Author

esmbc -- Efficient model checking with CI techniques

Map2Check -- fuzzing and symbolic execution

nesCheck -- good performance on subset of C

dckc Feb 4, 2021 Collaborator Author

dckc Feb 11, 2021 Collaborator Author

dckc Feb 22, 2021 Collaborator Author

dckc Mar 2, 2021 Collaborator Author

dckc Mar 2, 2021 Collaborator Author

dckc Apr 11, 2021 Collaborator Author

safety, metering via WASM?

zmanian Apr 11, 2021

dtribble Apr 11, 2021 Maintainer

safety, metering via WASM?

dckc Apr 12, 2021 Collaborator Author

dckc
Jan 20, 2021
Collaborator

dckc
Jan 20, 2021
Collaborator Author

dckc
Jan 20, 2021
Collaborator Author

erights
Jan 20, 2021
Maintainer

dckc
Jan 22, 2021
Collaborator Author

dckc
Jan 24, 2021
Collaborator Author

dckc
Jan 27, 2021
Collaborator Author

dckc
Jan 28, 2021
Collaborator Author

erights
Jan 28, 2021
Maintainer

dckc
Feb 1, 2021
Collaborator Author

dckc
Feb 2, 2021
Collaborator Author

dckc
Feb 4, 2021
Collaborator Author

dckc
Feb 11, 2021
Collaborator Author

dckc
Feb 22, 2021
Collaborator Author

dckc
Mar 2, 2021
Collaborator Author

dckc
Mar 2, 2021
Collaborator Author

dckc
Apr 11, 2021
Collaborator Author

zmanian
Apr 11, 2021

dtribble
Apr 11, 2021
Maintainer

dckc
Apr 12, 2021
Collaborator Author