[Javapathfinder-user] About java.lang.UnsatisfiedLinkError

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 422-6466

Hi all,

When I used JavaPathFinder to verify a Java Class DHKeyAgreement3
(source code is attached at the end). I encountered an exception
listed below:

java.lang.UnsatisfiedLinkError: java.io.ObjectStreamClass.initNative (no pe=
er)
=09at java.io.ObjectStreamClass.<clinit>(java\io\ObjectStreamClass.java:133=
)
=09at java.io.ObjectStreamField.<init>(java\io\ObjectStreamField.java:71)
=09at java.io.ObjectStreamField.<init>(java\io\ObjectStreamField.java:45)
=09at java.math.BigInteger.<clinit>(java\math\BigInteger.java:3008)
=09at DHKeyAgreement3.<clinit>(DHKeyAgreement3.java:204)
=09at DHKeyAgreement3.main(DHKeyAgreement3.java:37)

----------------------------------- path to error (length: 1)
Transition #0 Thread #0
  DHKeyAgreement3.java:168     private static final byte
skip1024ModulusBytes[] =3D {
  DHKeyAgreement3.java:204     private static final BigInteger skip1024Modu=
lus
  [no source for: java\math\BigInteger.java]
  [no source for: java\lang\Number.java]
  [no source for: java\lang\Object.java]
=09......

------------------------------------ end error path

=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
  1 Error Found: uncaught exception
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

I guess the exception was thrown because the JPF cannot find an
appropriate native peer class for java.io.ObjectStreamClass (JPF don't
provide this native peer class). If it is right, can I create a native
peer class for it to eliminate the exception? And if I can, can I do
it as the following:
(1) create a MJI model class for java.io.ObjectStreamClass and put it
in the env\jpf folder
(2) use "GenPeer" to generate a native peer class for
java.io.ObjectStreamClass and put in the env\jvm folder
?  Or it there any other solution? Is there any related documentation
on it? Thanks in advance for your help.

En

The source code of DHKeyAgreement3 class
/*
 * Copyright 1997-2001 by Sun Microsystems, Inc.,
 * 901 San Antonio Road, Palo Alto, California, 94303, U.S.A.
 * All rights reserved.
 *
 * This software is the confidential and proprietary information
 * of Sun Microsystems, Inc. ("Confidential Information").  You
 * shall not disclose such Confidential Information and shall use
 * it only in accordance with the terms of the license agreement
 * you entered into with Sun.
 */

import java.io.*;
import java.math.BigInteger;
import java.security.*;
import java.security.spec.*;
import java.security.interfaces.*;
import javax.crypto.*;
import javax.crypto.spec.*;
import javax.crypto.interfaces.*;
import com.sun.crypto.provider.SunJCE;

/**
 * This program executes the Diffie-Hellman key agreement protocol
 * between 3 parties: Alice, Bob, and Carol.
 *
 * We use the same 1024-bit prime modulus and base generator that are=20
 * used by SKIP.
 */

public class DHKeyAgreement3 {

    private DHKeyAgreement3() {}

    public static void main(String argv[]) {
        try {
            DHKeyAgreement3 keyAgree =3D new DHKeyAgreement3();
            keyAgree.run();
        } catch (Exception e) {
            System.err.println("Error: " + e);
            System.exit(1);
        }
    }

    private void run() throws Exception {

        DHParameterSpec dhSkipParamSpec;

        System.out.println("Using SKIP Diffie-Hellman parameters");
        dhSkipParamSpec =3D new DHParameterSpec(skip1024Modulus, skip1024Ba=
se);

        // Alice creates her own DH key pair
        System.out.println("ALICE: Generate DH keypair ...");
        KeyPairGenerator aliceKpairGen =3D KeyPairGenerator.getInstance("DH=
");
        aliceKpairGen.initialize(dhSkipParamSpec);
        KeyPair aliceKpair =3D aliceKpairGen.generateKeyPair();

        // Bob creates his own DH key pair
        System.out.println("BOB: Generate DH keypair ...");
        KeyPairGenerator bobKpairGen =3D KeyPairGenerator.getInstance("DH")=
;
        bobKpairGen.initialize(dhSkipParamSpec);
        KeyPair bobKpair =3D bobKpairGen.generateKeyPair();

        // Carol creates her own DH key pair
        System.out.println("CAROL: Generate DH keypair ...");
        KeyPairGenerator carolKpairGen =3D KeyPairGenerator.getInstance("DH=
");
        carolKpairGen.initialize(dhSkipParamSpec);
        KeyPair carolKpair =3D carolKpairGen.generateKeyPair();

        // Alice initialize
        System.out.println("ALICE: Initialize ...");
        KeyAgreement aliceKeyAgree =3D KeyAgreement.getInstance("DH");
        aliceKeyAgree.init(aliceKpair.getPrivate());

        // Bob initialize
        System.out.println("BOB: Initialize ...");
        KeyAgreement bobKeyAgree =3D KeyAgreement.getInstance("DH");
        bobKeyAgree.init(bobKpair.getPrivate());

        // Carol initialize
        System.out.println("CAROL: Initialize ...");
        KeyAgreement carolKeyAgree =3D KeyAgreement.getInstance("DH");
        carolKeyAgree.init(carolKpair.getPrivate());

        // Alice uses Carol's public key
        Key ac =3D aliceKeyAgree.doPhase(carolKpair.getPublic(), false);

        // Bob uses Alice's public key
        Key ba =3D bobKeyAgree.doPhase(aliceKpair.getPublic(), false);

        // Carol uses Bob's public key
        Key cb =3D carolKeyAgree.doPhase(bobKpair.getPublic(), false);

        // Alice uses Carol's result from above
        aliceKeyAgree.doPhase(cb, true);

        // Bob uses Alice's result from above
        bobKeyAgree.doPhase(ac, true);

        // Carol uses Bob's result from above
        carolKeyAgree.doPhase(ba, true);

        // Alice, Bob and Carol compute their secrets
        byte[] aliceSharedSecret =3D aliceKeyAgree.generateSecret();
        System.out.println("Alice secret: " + toHexString(aliceSharedSecret=
));

        byte[] bobSharedSecret =3D bobKeyAgree.generateSecret();
        System.out.println("Bob secret: " + toHexString(bobSharedSecret));

        byte[] carolSharedSecret =3D carolKeyAgree.generateSecret();
        System.out.println("Carol secret: " + toHexString(carolSharedSecret=
));

        // Compare Alice and Bob
        if (!java.util.Arrays.equals(aliceSharedSecret, bobSharedSecret))
            throw new Exception("Alice and Bob differ");
        System.out.println("Alice and Bob are the same");

        // Compare Bob and Carol
        if (!java.util.Arrays.equals(bobSharedSecret, carolSharedSecret))
            throw new Exception("Bob and Carol differ");
        System.out.println("Bob and Carol are the same");
    }

    /*
     * Converts a byte to hex digit and writes to the supplied buffer
     */
    private void byte2hex(byte b, StringBuffer buf) {
        char[] hexChars =3D { '0', '1', '2', '3', '4', '5', '6', '7', '8',
                            '9', 'A', 'B', 'C', 'D', 'E', 'F' };
        int high =3D ((b & 0xf0) >> 4);
        int low =3D (b & 0x0f);
        buf.append(hexChars[high]);
        buf.append(hexChars[low]);
    }

    /*
     * Converts a byte array to hex string
     */
    private String toHexString(byte[] block) {
        StringBuffer buf =3D new StringBuffer();

        int len =3D block.length;

        for (int i =3D 0; i < len; i++) {
             byte2hex(block[i], buf);
             if (i < len-1) {
                 buf.append(":");
             }
        }=20
        return buf.toString();
    }

    /*
     * Prints the usage of this test.
     */
    private void usage() {
        System.err.print("DHKeyAgreement usage: ");
        System.err.println("[-gen]");
    }

    // The 1024 bit Diffie-Hellman modulus values used by SKIP
    private static final byte skip1024ModulusBytes[] =3D {
        (byte)0xF4, (byte)0x88, (byte)0xFD, (byte)0x58,
        (byte)0x4E, (byte)0x49, (byte)0xDB, (byte)0xCD,
        (byte)0x20, (byte)0xB4, (byte)0x9D, (byte)0xE4,
        (byte)0x91, (byte)0x07, (byte)0x36, (byte)0x6B,
        (byte)0x33, (byte)0x6C, (byte)0x38, (byte)0x0D,
        (byte)0x45, (byte)0x1D, (byte)0x0F, (byte)0x7C,
        (byte)0x88, (byte)0xB3, (byte)0x1C, (byte)0x7C,
        (byte)0x5B, (byte)0x2D, (byte)0x8E, (byte)0xF6,
        (byte)0xF3, (byte)0xC9, (byte)0x23, (byte)0xC0,
        (byte)0x43, (byte)0xF0, (byte)0xA5, (byte)0x5B,
        (byte)0x18, (byte)0x8D, (byte)0x8E, (byte)0xBB,
        (byte)0x55, (byte)0x8C, (byte)0xB8, (byte)0x5D,
        (byte)0x38, (byte)0xD3, (byte)0x34, (byte)0xFD,
        (byte)0x7C, (byte)0x17, (byte)0x57, (byte)0x43,
        (byte)0xA3, (byte)0x1D, (byte)0x18, (byte)0x6C,
        (byte)0xDE, (byte)0x33, (byte)0x21, (byte)0x2C,
        (byte)0xB5, (byte)0x2A, (byte)0xFF, (byte)0x3C,
        (byte)0xE1, (byte)0xB1, (byte)0x29, (byte)0x40,
        (byte)0x18, (byte)0x11, (byte)0x8D, (byte)0x7C,
        (byte)0x84, (byte)0xA7, (byte)0x0A, (byte)0x72,
        (byte)0xD6, (byte)0x86, (byte)0xC4, (byte)0x03,
        (byte)0x19, (byte)0xC8, (byte)0x07, (byte)0x29,
        (byte)0x7A, (byte)0xCA, (byte)0x95, (byte)0x0C,
        (byte)0xD9, (byte)0x96, (byte)0x9F, (byte)0xAB,
        (byte)0xD0, (byte)0x0A, (byte)0x50, (byte)0x9B,
        (byte)0x02, (byte)0x46, (byte)0xD3, (byte)0x08,
        (byte)0x3D, (byte)0x66, (byte)0xA4, (byte)0x5D,
        (byte)0x41, (byte)0x9F, (byte)0x9C, (byte)0x7C,
        (byte)0xBD, (byte)0x89, (byte)0x4B, (byte)0x22,
        (byte)0x19, (byte)0x26, (byte)0xBA, (byte)0xAB,
        (byte)0xA2, (byte)0x5E, (byte)0xC3, (byte)0x55,
        (byte)0xE9, (byte)0x2F, (byte)0x78, (byte)0xC7
    };

    // The SKIP 1024 bit modulus
    private static final BigInteger skip1024Modulus
    =3D new BigInteger(1, skip1024ModulusBytes);

    // The base used with the SKIP 1024 bit modulus
    private static final BigInteger skip1024Base =3D BigInteger.valueOf(2);
}