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

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

@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.
cc @warner @dtribble @kriskowal

dump of open tabs:

javascript formal semantics - Google Search
Memory safety - Wikipedia
What is memory safety? - The PL Enthusiast
The Meaning of Memory Safety
- "Capability-based memory safety is a form of type safety with two
  types: pointer-types and scalars." -- Prof. Mathias Payer Spring 2017
- CS527 Software Security
What is Memory Safety in Programming? | by Arun Rajeevan | Medium
KJS: A Complete Formal Semantics of JavaScript - FSL
javascript-semantics/README.md at master · kframework/javascript-semantics
Certified semantics and analysis of JavaScript
An Operational Semantics for JavaScript
A Structural Operational Semantics for JavaScript

The text was updated successfully, but these errors were encountered:

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

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.

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

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.

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

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

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

for reference, earlier discussions:

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

cc @erights

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

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

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

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.

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

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 :).

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

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.

dckc transferred this issue from dckc/madmode-blog Jan 20, 2021

dckc transferred this issue from another repository Jan 20, 2021

dckc mentioned this issue Feb 19, 2021

unbounded heap growth crashes xst, xsnap (SIGSEGV) Moddable-OpenSource/moddable#567

Closed

This was referenced Mar 4, 2021

XS library security audit definition #2467

Closed

stack-overflow(fxBinaryExpressionNodeDistribute) Moddable-OpenSource/moddable#587

Closed

dckc mentioned this issue Apr 11, 2021

metering support in vat workers (XS regex, ...) #2322

Closed

dckc self-assigned this Apr 14, 2021

warner added the xsnap the XS execution tool label Apr 26, 2021

dckc added the security label May 3, 2021

dckc added this to the XS Memory Safety Audit milestone Jul 21, 2021

Tartuffo removed this from the XS Memory Safety Audit milestone Feb 8, 2022

Tartuffo added migrate-icebox and removed migrate-icebox labels Nov 17, 2022

Agoric locked and limited conversation to collaborators May 27, 2023

dckc converted this issue into discussion #7858 May 27, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

This issue was moved to a discussion.

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

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

dckc commented Jan 20, 2021 •

edited

Loading

dckc commented Jan 20, 2021

Pointers as capabilities

dckc commented Jan 20, 2021 •

edited

Loading

erights commented Jan 20, 2021 via email •

edited by dckc

Loading

dckc commented Jan 22, 2021

dckc commented Jan 24, 2021 •

edited

Loading

dckc commented Jan 27, 2021 •

edited

Loading

dckc commented Jan 28, 2021

erights commented Jan 28, 2021

dckc commented Feb 1, 2021 •

edited

Loading

dckc commented Feb 2, 2021 •

edited

Loading

dckc commented Feb 4, 2021

dckc commented Feb 11, 2021 •

edited

Loading

dckc commented Feb 22, 2021

dckc commented Mar 2, 2021 •

edited

Loading

dckc commented Mar 2, 2021

dckc commented Apr 11, 2021 •

edited

Loading

zmanian commented Apr 11, 2021

dtribble commented Apr 11, 2021 •

edited

Loading

safety, metering via WASM?

dckc commented Apr 12, 2021

This issue was moved to a discussion.

This issue was moved to a discussion.

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

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

Comments

dckc commented Jan 20, 2021 • edited Loading

dckc commented Jan 20, 2021

Hardware support? MPX in Intel Skylake

Pointers as capabilities

dckc commented Jan 20, 2021 • edited Loading

Executable: 1.5M

Compiled C: 2,084KB

Dependencies: libc, libpthread only

strcpy

erights commented Jan 20, 2021 via email • edited by dckc Loading

dckc commented Jan 22, 2021

dckc commented Jan 24, 2021 • edited Loading

SAFECode

Checked C looks active

dckc commented Jan 27, 2021 • edited Loading

fuzzing

dckc commented Jan 28, 2021

getters and setters vs. static analysis

erights commented Jan 28, 2021

dckc commented Feb 1, 2021 • edited Loading

setjmp / longjump

dckc commented Feb 2, 2021 • edited Loading

esmbc -- Efficient model checking with CI techniques

Map2Check -- fuzzing and symbolic execution

nesCheck -- good performance on subset of C

dckc commented Feb 4, 2021

dckc commented Feb 11, 2021 • edited Loading

dckc commented Feb 22, 2021

dckc commented Mar 2, 2021 • edited Loading

dckc commented Mar 2, 2021

dckc commented Apr 11, 2021 • edited Loading

safety, metering via WASM?

zmanian commented Apr 11, 2021

dtribble commented Apr 11, 2021 • edited Loading

safety, metering via WASM?

dckc commented Apr 12, 2021

This issue was moved to a discussion.

dckc commented Jan 20, 2021 •

edited

Loading

dckc commented Jan 20, 2021 •

edited

Loading

erights commented Jan 20, 2021 via email •

edited by dckc

Loading

dckc commented Jan 24, 2021 •

edited

Loading

dckc commented Jan 27, 2021 •

edited

Loading

dckc commented Feb 1, 2021 •

edited

Loading

dckc commented Feb 2, 2021 •

edited

Loading

dckc commented Feb 11, 2021 •

edited

Loading

dckc commented Mar 2, 2021 •

edited

Loading

dckc commented Apr 11, 2021 •

edited

Loading

dtribble commented Apr 11, 2021 •

edited

Loading