Sebyla Platform Specification

Constantine Plotnikov

Abstract

This document describes sebyla platform. Document is under construction and revision history is not maintained.

Table of Contents

1. Introduction
2. Sebyla Type System
Overview
Type resolution
Values and Variables
Template types
3. Sebyla Assembly File Format
Overview
4. Instructions for operations
Overview
Fundamental intsturctions
push.local
5. Support of non native programming languages
Overview
A. Glossary

Chapter 1. Introduction

Sebyla stands for SEcure BYtecode LAnguage. Sebyla platform is based on capability security model. This security model is most flexible of avialble ones. This model is different from ACL+Stack inspection model in Java and ECMA CLI.

Chapter 2. Sebyla Type System

Overview

Sebyla type system borrows from Java, C#, ML and many other programming languages. Primary purpose is to support capability based security and do not facilitate leaking any authority.

Types are devided in following major categories:

Type categories

Object types

These types are objects that are allocated on heap.

User definable object types

These types could bee definied by user.

interface types

These types declaring method signatures of methods of object but does not define state or behaviour.

class types

These types could define both state and behaviour.

build-in object types

These types are not normaly provided by user, they are usually implemented by virtual machine or compilier. Some of those types could be completly implemented in assembler or XCL, other require support from virtual machine.

array types

These types are fixed size colleciton of values. that are accessible by index. There are two kinds of arrays. MutableArray and VaulueArray

boxed value types

These types holds single value of value type. There are mutable and immutbable boxed types. Mutable boxes are T.Boxed immutable boxed are T.BoxedMutable These typse theoretically could be defined by user, but due their sinergy with value types they are implented by compiler.

Behaviour types

These types represent different forms of pointers to function. While they could be easily defined by user, they play important role in virtual machine, so they are considered as build in types.

Value types

These types are allocated on stack or embedding object.

User definable value types

These types could bee definied by user.

compound types(structs)

These types are composed of other values.

enumeration types

These types define list of integer constants.

build-in value types

These types are not normaly provided by user, they are usually implemented by virtual machine or compilier. Some of those types could be completly implemented in assembler or XCL, other require support from virtual machine.

primite value types

Thise types are primitive values like character, numbers.

LValue types

Thise are types that could participiate in assigment operations.

managed reference type (Ref[T],&T)

This type is managed reference to some variable or its field.

There are two principal category of types in sebyla system. Structure types which state is kept in place where thier location is declared and object types are types which state is resides somewhere else.

Structure types are also that one exact type and type convertion will involve copying values. On other hand, object types could have different type facets, their type could be widened or narrowed.

Type resolution

Before types could be used, there is type resolution stage, on this stage, all types which are resolved to thier actual syntax.

There are also alias types. These types are resolved to some specific types at class loading time. Their primary usage is to help with development as they provide additional level of indirection. alias types could be considered as type constants.

There are also template types. Template types are resolved at the stage of class loadeing.

Template types are loaded in lowest app domain context where all participiating types is loaded.

Resolved template type are not avaialbe in listing Assembly.GetTypes()

Values and Variables

Every context have number of names defined. Every name have an associated value. If name have been declared with "val" statement (or with assigment in method) it denotes assigned value. If value were declared with var statement it is denotes location so is of Ref[T] type.

In the object var declares variable, val declares constant, slot declares property that have modifier methods.

Mutable arrays and value arrays are two different things. Both have indexed get operation. For mutable arrays it returns Ref[T], for value arrays it return T. Array[T] implement ISequence[T] interface, Mutalble array implements, ISequence[Ref[T]] interface and hiddenly implmenets ISequence[T] interface.

Template types

Template differ depending whether they are for template value types or template reference types.

Template reference types support covariance. for example Array[string] could be casted to Array[object]. Instanceof will also react accordingly

Template reference types support covariance from value to boxed type. For example HashMap[int,int] could be casted to HashMap[int,int.Boxed] or to HashMap[object,object] or to IMap[int,int].

This works because of private types on object.

Full implementation for N-parameter tempalte with M interfaces and superclasses types with values will need (2N+1-1)*M type objects. If compiled to C, only needed types need to be supported, so this number will be less. Also not that most template types in collection library have 1-2 arguments and about 3 interfaces or superclasses. For example HashMap have IMap interface, AbstractMap base class and IEnumberable interface. So cost of full implementation of HashMap[int,int] is ((2**3)-1)*3 which is 21 type object. Most likely static analisys will eliminate most of this const. Also likely efficient implemenation of those types could be generted on as needed basis.

Because of covariance it is not important if Map[int,int] will be implemented with Map[int.Boxed, int.Boxed] or not. Implementation of template of values with boxed types will allow to have one implementation for all, but which will not be very efficient.

It would be even possible to choose implementation on fly as dinamyc optimization.

Chapter 3. Sebyla Assembly File Format

Table of Contents

Overview

Overview

Here will be a description of assembly file format.

Chapter 4. Instructions for operations

Overview

There are fundamental and macro instructions. Set of fundametal bytecode instructions is enough to express full functionality of virtual machine. Macro instructions could be expressed using fundametal instructions and usually provide optimization hint that could be used by jit compilers or interpreters.

Fundamental intsturctions

push.local

This operation takes local value an pushes it on stack.

Chapter 5. Support of non native programming languages

Table of Contents

Overview

Overview

While Sebyla platform is reasonably rich, it have been desinged to support one particular language XCL. Other langauges with simlar memory and execution model could be supported, but their security model will need to be bridged to sebyla. This could be still reasonable to do so in order to provide confined runtimes for those other languages and to be able prove security properties of that langauges.

This chapter will discuss different techniques that could be used those non native languages.

Appendix A. Glossary

Table of Contents

Glossary

Glossary

A

Assembly

A code distribution unit. Assembly is single file. Classes in one assembly could access "internal" members of each other.

S

Sebyla

Secure bytecode language.

T

Type

A description of all possible opertions on value.

X

XCL

Extensible Capability Language. High level langauge for Sebyla platform.